kmlem12 - Metamath Proof Explorer

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

Theorem kmlem12 8541

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 3062	. . . 4 $\$ $\$
3		df-ral 2819	. . . 4 $\$ $\$ $\$ $\$
4		vex 3116	. . . . . . . . 9
5		eqeq1 2471	. . . . . . . . . 10 $\$ $\$ $\$ $\$
6	5	rexbidv 2973	. . . . . . . . 9 $\$ $\$ $\$ $\$
7	4, 6	elab 3250	. . . . . . . 8 $\$ $\$ $\$ $\$
8	7	imbi1i 325	. . . . . . 7 $\$ $\$ $\$ $\$
9		r19.23v 2943	. . . . . . 7 $\$ $\$ $\$ $\$
10	8, 9	bitr4i 252	. . . . . 6 $\$ $\$ $\$ $\$
11	10	albii 1620	. . . . 5 $\$ $\$ $\$ $\$
12		ralcom4 3132	. . . . 5 $\$ $\$ $\$ $\$
13		vex 3116	. . . . . . . 8
14		difexg 4595	. . . . . . . 8 $\$ $\$
15	13, 14	ax-mp 5	. . . . . . 7 $\$ $\$
16		neeq1 2748	. . . . . . . 8 $\$ $\$ $\$ $\$
17		ineq1 3693	. . . . . . . . . 10 $\$ $\$ $\$ $\$
18	17	eleq2d 2537	. . . . . . . . 9 $\$ $\$ $\$ $\$
19	18	eubidv 2298	. . . . . . . 8 $\$ $\$ $\$ $\$
20	16, 19	imbi12d 320	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
21	15, 20	ceqsalv 3141	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
22	21	ralbii 2895	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
23	11, 12, 22	3bitr2i 273	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
24	2, 3, 23	3bitri 271	. . 3 $\$ $\$ $\$ $\$
25		ralim 2853	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	24, 25	sylbi 195	. 2 $\$ $\$ $\$ $\$
27		difeq1 3615	. . . . . . . 8 $\$ $\$ $\$ $\$
28		sneq 4037	. . . . . . . . . . 11
29	28	difeq2d 3622	. . . . . . . . . 10 $\$ $\$
30	29	unieqd 4255	. . . . . . . . 9 $\$ $\$
31	30	difeq2d 3622	. . . . . . . 8 $\$ $\$ $\$ $\$
32	27, 31	eqtrd 2508	. . . . . . 7 $\$ $\$ $\$ $\$
33	32	neeq1d 2744	. . . . . 6 $\$ $\$ $\$ $\$
34	33	cbvralv 3088	. . . . 5 $\$ $\$ $\$ $\$
35	32	ineq1d 3699	. . . . . . . 8 $\$ $\$ $\$ $\$
36	35	eleq2d 2537	. . . . . . 7 $\$ $\$ $\$ $\$
37	36	eubidv 2298	. . . . . 6 $\$ $\$ $\$ $\$
38	37	cbvralv 3088	. . . . 5 $\$ $\$ $\$ $\$
39	34, 38	imbi12i 326	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
40		in12 3709	. . . . . . . . . . 11
41		incom 3691	. . . . . . . . . . 11
42	40, 41	eqtri 2496	. . . . . . . . . 10
43	1	kmlem11 8540	. . . . . . . . . . 11 $\$ $\$
44	43	ineq1d 3699	. . . . . . . . . 10 $\$ $\$
45	42, 44	syl5req 2521	. . . . . . . . 9 $\$ $\$
46	45	eleq2d 2537	. . . . . . . 8 $\$ $\$
47	46	eubidv 2298	. . . . . . 7 $\$ $\$
48		ax-1 6	. . . . . . 7
49	47, 48	syl6bi 228	. . . . . 6 $\$ $\$
50	49	ralimia 2855	. . . . 5 $\$ $\$
51	50	imim2i 14	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
52	39, 51	sylbi 195	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
53	52	com12 31	. 2 $\$ $\$ $\$ $\$ $\$ $\$
54	26, 53	syl5 32	1 $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wal 1377

wceq 1379

wcel 1767

weu 2275

cab 2452

wne 2662

wral 2814

wrex 2815

cvv 3113 $\$ cdif 3473

cin 3475

c0 3785

csn 4027

cuni 4245

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-sn 4028 df-uni 4246 df-iun 4327

This theorem is referenced by: kmlem13 8542

W3C validator