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 8588

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		kmlem9.1	. . . . 5 $\$ $\$
2	1	raleqi 2990	. . . 4 $\$ $\$
3		df-ral 2741	. . . 4 $\$ $\$ $\$ $\$
4		vex 3047	. . . . . . . . 9
5		eqeq1 2454	. . . . . . . . . 10 $\$ $\$ $\$ $\$
6	5	rexbidv 2900	. . . . . . . . 9 $\$ $\$ $\$ $\$
7	4, 6	elab 3184	. . . . . . . 8 $\$ $\$ $\$ $\$
8	7	imbi1i 327	. . . . . . 7 $\$ $\$ $\$ $\$
9		r19.23v 2866	. . . . . . 7 $\$ $\$ $\$ $\$
10	8, 9	bitr4i 256	. . . . . 6 $\$ $\$ $\$ $\$
11	10	albii 1690	. . . . 5 $\$ $\$ $\$ $\$
12		ralcom4 3065	. . . . 5 $\$ $\$ $\$ $\$
13		vex 3047	. . . . . . . 8
14		difexg 4550	. . . . . . . 8 $\$ $\$
15	13, 14	ax-mp 5	. . . . . . 7 $\$ $\$
16		neeq1 2685	. . . . . . . 8 $\$ $\$ $\$ $\$
17		ineq1 3626	. . . . . . . . . 10 $\$ $\$ $\$ $\$
18	17	eleq2d 2513	. . . . . . . . 9 $\$ $\$ $\$ $\$
19	18	eubidv 2318	. . . . . . . 8 $\$ $\$ $\$ $\$
20	16, 19	imbi12d 322	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
21	15, 20	ceqsalv 3074	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
22	21	ralbii 2818	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
23	11, 12, 22	3bitr2i 277	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
24	2, 3, 23	3bitri 275	. . 3 $\$ $\$ $\$ $\$
25		ralim 2776	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	24, 25	sylbi 199	. 2 $\$ $\$ $\$ $\$
27		difeq1 3543	. . . . . . . 8 $\$ $\$ $\$ $\$
28		sneq 3977	. . . . . . . . . . 11
29	28	difeq2d 3550	. . . . . . . . . 10 $\$ $\$
30	29	unieqd 4207	. . . . . . . . 9 $\$ $\$
31	30	difeq2d 3550	. . . . . . . 8 $\$ $\$ $\$ $\$
32	27, 31	eqtrd 2484	. . . . . . 7 $\$ $\$ $\$ $\$
33	32	neeq1d 2682	. . . . . 6 $\$ $\$ $\$ $\$
34	33	cbvralv 3018	. . . . 5 $\$ $\$ $\$ $\$
35	32	ineq1d 3632	. . . . . . . 8 $\$ $\$ $\$ $\$
36	35	eleq2d 2513	. . . . . . 7 $\$ $\$ $\$ $\$
37	36	eubidv 2318	. . . . . 6 $\$ $\$ $\$ $\$
38	37	cbvralv 3018	. . . . 5 $\$ $\$ $\$ $\$
39	34, 38	imbi12i 328	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
40		in12 3642	. . . . . . . . . . 11
41		incom 3624	. . . . . . . . . . 11
42	40, 41	eqtri 2472	. . . . . . . . . 10
43	1	kmlem11 8587	. . . . . . . . . . 11 $\$ $\$
44	43	ineq1d 3632	. . . . . . . . . 10 $\$ $\$
45	42, 44	syl5req 2497	. . . . . . . . 9 $\$ $\$
46	45	eleq2d 2513	. . . . . . . 8 $\$ $\$
47	46	eubidv 2318	. . . . . . 7 $\$ $\$
48		ax-1 6	. . . . . . 7
49	47, 48	syl6bi 232	. . . . . 6 $\$ $\$
50	49	ralimia 2778	. . . . 5 $\$ $\$
51	50	imim2i 16	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
52	39, 51	sylbi 199	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
53	52	com12 32	. 2 $\$ $\$ $\$ $\$ $\$ $\$
54	26, 53	syl5 33	1 $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wal 1441

wceq 1443

wcel 1886

weu 2298

cab 2436

wne 2621

wral 2736

wrex 2737

cvv 3044 $\$ cdif 3400

cin 3402

c0 3730

csn 3967

cuni 4197

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-sbc 3267 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-sn 3968 df-uni 4198 df-iun 4279

This theorem is referenced by: kmlem13 8589

W3C validator