kmlem12 - Metamath Proof Explorer

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

Theorem kmlem12 8330

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 2921	. . . 4 $\$ $\$
3		df-ral 2720	. . . 4 $\$ $\$ $\$ $\$
4		vex 2975	. . . . . . . . 9
5		eqeq1 2449	. . . . . . . . . 10 $\$ $\$ $\$ $\$
6	5	rexbidv 2736	. . . . . . . . 9 $\$ $\$ $\$ $\$
7	4, 6	elab 3106	. . . . . . . 8 $\$ $\$ $\$ $\$
8	7	imbi1i 325	. . . . . . 7 $\$ $\$ $\$ $\$
9		r19.23v 2833	. . . . . . 7 $\$ $\$ $\$ $\$
10	8, 9	bitr4i 252	. . . . . 6 $\$ $\$ $\$ $\$
11	10	albii 1610	. . . . 5 $\$ $\$ $\$ $\$
12		ralcom4 2991	. . . . 5 $\$ $\$ $\$ $\$
13		vex 2975	. . . . . . . 8
14		difexg 4440	. . . . . . . 8 $\$ $\$
15	13, 14	ax-mp 5	. . . . . . 7 $\$ $\$
16		neeq1 2616	. . . . . . . 8 $\$ $\$ $\$ $\$
17		ineq1 3545	. . . . . . . . . 10 $\$ $\$ $\$ $\$
18	17	eleq2d 2510	. . . . . . . . 9 $\$ $\$ $\$ $\$
19	18	eubidv 2276	. . . . . . . 8 $\$ $\$ $\$ $\$
20	16, 19	imbi12d 320	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
21	15, 20	ceqsalv 3000	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
22	21	ralbii 2739	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
23	11, 12, 22	3bitr2i 273	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$
24	2, 3, 23	3bitri 271	. . 3 $\$ $\$ $\$ $\$
25		ralim 2787	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	24, 25	sylbi 195	. 2 $\$ $\$ $\$ $\$
27		difeq1 3467	. . . . . . . 8 $\$ $\$ $\$ $\$
28		sneq 3887	. . . . . . . . . . 11
29	28	difeq2d 3474	. . . . . . . . . 10 $\$ $\$
30	29	unieqd 4101	. . . . . . . . 9 $\$ $\$
31	30	difeq2d 3474	. . . . . . . 8 $\$ $\$ $\$ $\$
32	27, 31	eqtrd 2475	. . . . . . 7 $\$ $\$ $\$ $\$
33	32	neeq1d 2621	. . . . . 6 $\$ $\$ $\$ $\$
34	33	cbvralv 2947	. . . . 5 $\$ $\$ $\$ $\$
35	32	ineq1d 3551	. . . . . . . 8 $\$ $\$ $\$ $\$
36	35	eleq2d 2510	. . . . . . 7 $\$ $\$ $\$ $\$
37	36	eubidv 2276	. . . . . 6 $\$ $\$ $\$ $\$
38	37	cbvralv 2947	. . . . 5 $\$ $\$ $\$ $\$
39	34, 38	imbi12i 326	. . . 4 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
40		in12 3561	. . . . . . . . . . 11
41		incom 3543	. . . . . . . . . . 11
42	40, 41	eqtri 2463	. . . . . . . . . 10
43	1	kmlem11 8329	. . . . . . . . . . 11 $\$ $\$
44	43	ineq1d 3551	. . . . . . . . . 10 $\$ $\$
45	42, 44	syl5req 2488	. . . . . . . . 9 $\$ $\$
46	45	eleq2d 2510	. . . . . . . 8 $\$ $\$
47	46	eubidv 2276	. . . . . . 7 $\$ $\$
48		ax-1 6	. . . . . . 7
49	47, 48	syl6bi 228	. . . . . 6 $\$ $\$
50	49	ralimia 2789	. . . . 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 1367

wceq 1369

wcel 1756

weu 2253

cab 2429

wne 2606

wral 2715

wrex 2716

cvv 2972 $\$ cdif 3325

cin 3327

c0 3637

csn 3877

cuni 4091

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-rab 2724 df-v 2974 df-sbc 3187 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-sn 3878 df-uni 4092 df-iun 4173

This theorem is referenced by: kmlem13 8331

W3C validator