kmlem12 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > kmlem12		Structured version Visualization version Unicode version

Theorem kmlem12 8983

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004.)

**Hypothesis**
Ref	Expression
kmlem9.1	$\$ $\$

**Assertion**
Ref	Expression
kmlem12	$\$ $\$

Distinct variable groups:

Allowed substitution hints:

(

)

**Proof of Theorem kmlem12**
Step	Hyp	Ref	Expression
1		difeq1 3721	. . . . . . 7 $\$ $\$ $\$ $\$
2		sneq 4187	. . . . . . . . . 10
3	2	difeq2d 3728	. . . . . . . . 9 $\$ $\$
4	3	unieqd 4446	. . . . . . . 8 $\$ $\$
5	4	difeq2d 3728	. . . . . . 7 $\$ $\$ $\$ $\$
6	1, 5	eqtrd 2656	. . . . . 6 $\$ $\$ $\$ $\$
7	6	neeq1d 2853	. . . . 5 $\$ $\$ $\$ $\$
8	7	cbvralv 3171	. . . 4 $\$ $\$ $\$ $\$
9	6	ineq1d 3813	. . . . . . 7 $\$ $\$ $\$ $\$
10	9	eleq2d 2687	. . . . . 6 $\$ $\$ $\$ $\$
11	10	eubidv 2490	. . . . 5 $\$ $\$ $\$ $\$
12	11	cbvralv 3171	. . . 4 $\$ $\$ $\$ $\$
13	8, 12	imbi12i 340	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
14		in12 3824	. . . . . . . . . 10
15		incom 3805	. . . . . . . . . 10
16	14, 15	eqtri 2644	. . . . . . . . 9
17		kmlem9.1	. . . . . . . . . . 11 $\$ $\$
18	17	kmlem11 8982	. . . . . . . . . 10 $\$ $\$
19	18	ineq1d 3813	. . . . . . . . 9 $\$ $\$
20	16, 19	syl5req 2669	. . . . . . . 8 $\$ $\$
21	20	eleq2d 2687	. . . . . . 7 $\$ $\$
22	21	eubidv 2490	. . . . . 6 $\$ $\$
23		ax-1 6	. . . . . 6
24	22, 23	syl6bi 243	. . . . 5 $\$ $\$
25	24	ralimia 2950	. . . 4 $\$ $\$
26	25	imim2i 16	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
27	13, 26	sylbi 207	. 2 $\$ $\$ $\$ $\$ $\$ $\$
28	17	raleqi 3142	. . . 4 $\$ $\$
29		df-ral 2917	. . . 4 $\$ $\$ $\$ $\$
30		vex 3203	. . . . . . . . 9
31		eqeq1 2626	. . . . . . . . . 10 $\$ $\$ $\$ $\$
32	31	rexbidv 3052	. . . . . . . . 9 $\$ $\$ $\$ $\$
33	30, 32	elab 3350	. . . . . . . 8 $\$ $\$ $\$ $\$
34	33	imbi1i 339	. . . . . . 7 $\$ $\$ $\$ $\$
35		r19.23v 3023	. . . . . . 7 $\$ $\$ $\$ $\$
36	34, 35	bitr4i 267	. . . . . 6 $\$ $\$ $\$ $\$
37	36	albii 1747	. . . . 5 $\$ $\$ $\$ $\$
38		ralcom4 3224	. . . . 5 $\$ $\$ $\$ $\$
39		vex 3203	. . . . . . . 8
40	39	difexi 4809	. . . . . . 7 $\$ $\$
41		neeq1 2856	. . . . . . . 8 $\$ $\$ $\$ $\$
42		ineq1 3807	. . . . . . . . . 10 $\$ $\$ $\$ $\$
43	42	eleq2d 2687	. . . . . . . . 9 $\$ $\$ $\$ $\$
44	43	eubidv 2490	. . . . . . . 8 $\$ $\$ $\$ $\$
45	41, 44	imbi12d 334	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
46	40, 45	ceqsalv 3233	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
47	46	ralbii 2980	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
48	37, 38, 47	3bitr2i 288	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
49	28, 29, 48	3bitri 286	. . 3 $\$ $\$ $\$ $\$
50		ralim 2948	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
51	49, 50	sylbi 207	. 2 $\$ $\$ $\$ $\$
52	27, 51	syl11 33	1 $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wal 1481

wceq 1483

wcel 1990

weu 2470

cab 2608

wne 2794

wral 2912

wrex 2913 $\$ cdif 3571

cin 3573

c0 3915

csn 4177

cuni 4436

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-sn 4178 df-uni 4437 df-iun 4522

This theorem is referenced by: kmlem13 8984

W3C validator