kmlem13 - Metamath Proof Explorer

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

Theorem kmlem13 8984

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 5-Apr-2004.)

**Hypothesis**
Ref	Expression
kmlem9.1	$\$ $\$

**Assertion**
Ref	Expression
kmlem13	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem kmlem13 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kmlem1 8972	. . 3 $/\$
2		raleq 3138	. . . . . . 7
3	2	raleqbi1dv 3146	. . . . . 6
4		raleq 3138	. . . . . . 7
5	4	exbidv 1850	. . . . . 6
6	3, 5	imbi12d 334	. . . . 5
7	6	cbvalv 2273	. . . 4
8		kmlem9.1	. . . . . . 7 $\$ $\$
9	8	kmlem10 8981	. . . . . 6
10		ineq2 3808	. . . . . . . . . . . 12
11	10	eleq2d 2687	. . . . . . . . . . 11
12	11	eubidv 2490	. . . . . . . . . 10
13	12	imbi2d 330	. . . . . . . . 9
14	13	ralbidv 2986	. . . . . . . 8
15	14	cbvexv 2275	. . . . . . 7
16		kmlem3 8974	. . . . . . . . . . 11 $\$ $\$
17		ralinexa 2997	. . . . . . . . . . . 12 $/\$
18	17	rexbii 3041	. . . . . . . . . . 11 $/\$
19		rexnal 2995	. . . . . . . . . . 11 $/\$ $/\$
20	16, 18, 19	3bitri 286	. . . . . . . . . 10 $\$ $\$ $/\$
21	20	ralbii 2980	. . . . . . . . 9 $\$ $\$ $/\$
22		ralnex 2992	. . . . . . . . 9 $/\$ $/\$
23	21, 22	bitri 264	. . . . . . . 8 $\$ $\$ $/\$
24	8	kmlem12 8983	. . . . . . . . . . 11 $\$ $\$
25		vex 3203	. . . . . . . . . . . . 13
26	25	inex1 4799	. . . . . . . . . . . 12
27		ineq2 3808	. . . . . . . . . . . . . . . 16
28	27	eleq2d 2687	. . . . . . . . . . . . . . 15
29	28	eubidv 2490	. . . . . . . . . . . . . 14
30	29	imbi2d 330	. . . . . . . . . . . . 13
31	30	ralbidv 2986	. . . . . . . . . . . 12
32	26, 31	spcev 3300	. . . . . . . . . . 11
33	24, 32	syl6 35	. . . . . . . . . 10 $\$ $\$
34	33	exlimdv 1861	. . . . . . . . 9 $\$ $\$
35	34	com12 32	. . . . . . . 8 $\$ $\$
36	23, 35	syl5bir 233	. . . . . . 7 $/\$
37	15, 36	sylbi 207	. . . . . 6 $/\$
38	9, 37	syl 17	. . . . 5 $/\$
39	38	alrimiv 1855	. . . 4 $/\$
40	7, 39	sylbi 207	. . 3 $/\$
41	1, 40	syl 17	. 2 $/\$ $/\$
42		kmlem7 8978	. . . . 5 $/\$ $/\$
43	42	imim1i 63	. . . 4 $/\$ $/\$
44		biimt 350	. . . . . . . . 9
45	44	ralimi 2952	. . . . . . . 8
46		ralbi 3068	. . . . . . . 8
47	45, 46	syl 17	. . . . . . 7
48	47	exbidv 1850	. . . . . 6
49	48	adantr 481	. . . . 5 $/\$
50	49	pm5.74i 260	. . . 4 $/\$ $/\$
51	43, 50	sylibr 224	. . 3 $/\$ $/\$
52	51	alimi 1739	. 2 $/\$ $/\$
53	41, 52	impbii 199	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wal 1481

wceq 1483

wex 1704

wcel 1990

weu 2470

cab 2608

wne 2794

wral 2912

wrex 2913 $\$ cdif 3571

cin 3573

c0 3915

csn 4177

cuni 4436

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896

This theorem is referenced by: dfackm 8988

W3C validator