kmlem12 - Metamath Proof Explorer

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

Theorem kmlem12 8326

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 2919	. . . 4 $\$ $\$
3		df-ral 2718	. . . 4 $\$ $\$ $\$ $\$
4		vex 2973	. . . . . . . . 9
5		eqeq1 2447	. . . . . . . . . 10 $\$ $\$ $\$ $\$
6	5	rexbidv 2734	. . . . . . . . 9 $\$ $\$ $\$ $\$
7	4, 6	elab 3103	. . . . . . . 8 $\$ $\$ $\$ $\$
8	7	imbi1i 325	. . . . . . 7 $\$ $\$ $\$ $\$
9		r19.23v 2831	. . . . . . 7 $\$ $\$ $\$ $\$
10	8, 9	bitr4i 252	. . . . . 6 $\$ $\$ $\$ $\$
11	10	albii 1615	. . . . 5 $\$ $\$ $\$ $\$
12		ralcom4 2989	. . . . 5 $\$ $\$ $\$ $\$
13		vex 2973	. . . . . . . 8
14		difexg 4437	. . . . . . . 8 $\$ $\$
15	13, 14	ax-mp 5	. . . . . . 7 $\$ $\$
16		neeq1 2614	. . . . . . . 8 $\$ $\$ $\$ $\$
17		ineq1 3542	. . . . . . . . . 10 $\$ $\$ $\$ $\$
18	17	eleq2d 2508	. . . . . . . . 9 $\$ $\$ $\$ $\$
19	18	eubidv 2281	. . . . . . . 8 $\$ $\$ $\$ $\$
20	16, 19	imbi12d 320	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
21	15, 20	ceqsalv 2997	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
22	21	ralbii 2737	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
23	11, 12, 22	3bitr2i 273	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
24	2, 3, 23	3bitri 271	. . 3 $\$ $\$ $\$ $\$
25		ralim 2785	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	24, 25	sylbi 195	. 2 $\$ $\$ $\$ $\$
27		difeq1 3464	. . . . . . . 8 $\$ $\$ $\$ $\$
28		sneq 3884	. . . . . . . . . . 11
29	28	difeq2d 3471	. . . . . . . . . 10 $\$ $\$
30	29	unieqd 4098	. . . . . . . . 9 $\$ $\$
31	30	difeq2d 3471	. . . . . . . 8 $\$ $\$ $\$ $\$
32	27, 31	eqtrd 2473	. . . . . . 7 $\$ $\$ $\$ $\$
33	32	neeq1d 2619	. . . . . 6 $\$ $\$ $\$ $\$
34	33	cbvralv 2945	. . . . 5 $\$ $\$ $\$ $\$
35	32	ineq1d 3548	. . . . . . . 8 $\$ $\$ $\$ $\$
36	35	eleq2d 2508	. . . . . . 7 $\$ $\$ $\$ $\$
37	36	eubidv 2281	. . . . . 6 $\$ $\$ $\$ $\$
38	37	cbvralv 2945	. . . . 5 $\$ $\$ $\$ $\$
39	34, 38	imbi12i 326	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
40		in12 3558	. . . . . . . . . . 11
41		incom 3540	. . . . . . . . . . 11
42	40, 41	eqtri 2461	. . . . . . . . . 10
43	1	kmlem11 8325	. . . . . . . . . . 11 $\$ $\$
44	43	ineq1d 3548	. . . . . . . . . 10 $\$ $\$
45	42, 44	syl5req 2486	. . . . . . . . 9 $\$ $\$
46	45	eleq2d 2508	. . . . . . . 8 $\$ $\$
47	46	eubidv 2281	. . . . . . 7 $\$ $\$
48		ax-1 6	. . . . . . 7
49	47, 48	syl6bi 228	. . . . . 6 $\$ $\$
50	49	ralimia 2787	. . . . 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 1362

wceq 1364

wcel 1761

weu 2259

cab 2427

wne 2604

wral 2713

wrex 2714

cvv 2970 $\$ cdif 3322

cin 3324

c0 3634

csn 3874

cuni 4088

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-sbc 3184 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-sn 3875 df-uni 4089 df-iun 4170

This theorem is referenced by: kmlem13 8327

W3C validator