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 8609

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 2977	. . . 4 $\$ $\$
3		df-ral 2761	. . . 4 $\$ $\$ $\$ $\$
4		vex 3034	. . . . . . . . 9
5		eqeq1 2475	. . . . . . . . . 10 $\$ $\$ $\$ $\$
6	5	rexbidv 2892	. . . . . . . . 9 $\$ $\$ $\$ $\$
7	4, 6	elab 3173	. . . . . . . 8 $\$ $\$ $\$ $\$
8	7	imbi1i 332	. . . . . . 7 $\$ $\$ $\$ $\$
9		r19.23v 2863	. . . . . . 7 $\$ $\$ $\$ $\$
10	8, 9	bitr4i 260	. . . . . 6 $\$ $\$ $\$ $\$
11	10	albii 1699	. . . . 5 $\$ $\$ $\$ $\$
12		ralcom4 3052	. . . . 5 $\$ $\$ $\$ $\$
13		vex 3034	. . . . . . . 8
14		difexg 4545	. . . . . . . 8 $\$ $\$
15	13, 14	ax-mp 5	. . . . . . 7 $\$ $\$
16		neeq1 2705	. . . . . . . 8 $\$ $\$ $\$ $\$
17		ineq1 3618	. . . . . . . . . 10 $\$ $\$ $\$ $\$
18	17	eleq2d 2534	. . . . . . . . 9 $\$ $\$ $\$ $\$
19	18	eubidv 2339	. . . . . . . 8 $\$ $\$ $\$ $\$
20	16, 19	imbi12d 327	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
21	15, 20	ceqsalv 3061	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
22	21	ralbii 2823	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
23	11, 12, 22	3bitr2i 281	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
24	2, 3, 23	3bitri 279	. . 3 $\$ $\$ $\$ $\$
25		ralim 2792	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	24, 25	sylbi 200	. 2 $\$ $\$ $\$ $\$
27		difeq1 3533	. . . . . . . 8 $\$ $\$ $\$ $\$
28		sneq 3969	. . . . . . . . . . 11
29	28	difeq2d 3540	. . . . . . . . . 10 $\$ $\$
30	29	unieqd 4200	. . . . . . . . 9 $\$ $\$
31	30	difeq2d 3540	. . . . . . . 8 $\$ $\$ $\$ $\$
32	27, 31	eqtrd 2505	. . . . . . 7 $\$ $\$ $\$ $\$
33	32	neeq1d 2702	. . . . . 6 $\$ $\$ $\$ $\$
34	33	cbvralv 3005	. . . . 5 $\$ $\$ $\$ $\$
35	32	ineq1d 3624	. . . . . . . 8 $\$ $\$ $\$ $\$
36	35	eleq2d 2534	. . . . . . 7 $\$ $\$ $\$ $\$
37	36	eubidv 2339	. . . . . 6 $\$ $\$ $\$ $\$
38	37	cbvralv 3005	. . . . 5 $\$ $\$ $\$ $\$
39	34, 38	imbi12i 333	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
40		in12 3634	. . . . . . . . . . 11
41		incom 3616	. . . . . . . . . . 11
42	40, 41	eqtri 2493	. . . . . . . . . 10
43	1	kmlem11 8608	. . . . . . . . . . 11 $\$ $\$
44	43	ineq1d 3624	. . . . . . . . . 10 $\$ $\$
45	42, 44	syl5req 2518	. . . . . . . . 9 $\$ $\$
46	45	eleq2d 2534	. . . . . . . 8 $\$ $\$
47	46	eubidv 2339	. . . . . . 7 $\$ $\$
48		ax-1 6	. . . . . . 7
49	47, 48	syl6bi 236	. . . . . 6 $\$ $\$
50	49	ralimia 2794	. . . . 5 $\$ $\$
51	50	imim2i 16	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
52	39, 51	sylbi 200	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
53	52	com12 31	. 2 $\$ $\$ $\$ $\$ $\$ $\$
54	26, 53	syl5 32	1 $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wal 1450

wceq 1452

wcel 1904

weu 2319

cab 2457

wne 2641

wral 2756

wrex 2757

cvv 3031 $\$ cdif 3387

cin 3389

c0 3722

csn 3959

cuni 4190

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-sn 3960 df-uni 4191 df-iun 4271

This theorem is referenced by: kmlem13 8610

W3C validator