kmlem13 - Metamath Proof Explorer

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

Theorem kmlem13 8343

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 8331	. . 3 $/\$
2		raleq 2929	. . . . . . 7
3	2	raleqbi1dv 2937	. . . . . 6
4		raleq 2929	. . . . . . 7
5	4	exbidv 1680	. . . . . 6
6	3, 5	imbi12d 320	. . . . 5
7	6	cbvalv 1971	. . . 4
8		kmlem9.1	. . . . . . 7 $\$ $\$
9	8	kmlem10 8340	. . . . . 6
10		ineq2 3558	. . . . . . . . . . . 12
11	10	eleq2d 2510	. . . . . . . . . . 11
12	11	eubidv 2276	. . . . . . . . . 10
13	12	imbi2d 316	. . . . . . . . 9
14	13	ralbidv 2747	. . . . . . . 8
15	14	cbvexv 1972	. . . . . . 7
16		kmlem3 8333	. . . . . . . . . . 11 $\$ $\$
17		ralinexa 2772	. . . . . . . . . . . 12 $/\$
18	17	rexbii 2752	. . . . . . . . . . 11 $/\$
19		rexnal 2738	. . . . . . . . . . 11 $/\$ $/\$
20	16, 18, 19	3bitri 271	. . . . . . . . . 10 $\$ $\$ $/\$
21	20	ralbii 2751	. . . . . . . . 9 $\$ $\$ $/\$
22		ralnex 2737	. . . . . . . . 9 $/\$ $/\$
23	21, 22	bitri 249	. . . . . . . 8 $\$ $\$ $/\$
24	8	kmlem12 8342	. . . . . . . . . . 11 $\$ $\$
25		vex 2987	. . . . . . . . . . . . 13
26	25	inex1 4445	. . . . . . . . . . . 12
27		ineq2 3558	. . . . . . . . . . . . . . . 16
28	27	eleq2d 2510	. . . . . . . . . . . . . . 15
29	28	eubidv 2276	. . . . . . . . . . . . . 14
30	29	imbi2d 316	. . . . . . . . . . . . 13
31	30	ralbidv 2747	. . . . . . . . . . . 12
32	26, 31	spcev 3076	. . . . . . . . . . 11
33	24, 32	syl6 33	. . . . . . . . . 10 $\$ $\$
34	33	exlimdv 1690	. . . . . . . . 9 $\$ $\$
35	34	com12 31	. . . . . . . 8 $\$ $\$
36	23, 35	syl5bir 218	. . . . . . 7 $/\$
37	15, 36	sylbi 195	. . . . . 6 $/\$
38	9, 37	syl 16	. . . . 5 $/\$
39	38	alrimiv 1685	. . . 4 $/\$
40	7, 39	sylbi 195	. . 3 $/\$
41	1, 40	syl 16	. 2 $/\$ $/\$
42		kmlem7 8337	. . . . 5 $/\$ $/\$
43	42	imim1i 58	. . . 4 $/\$ $/\$
44		biimt 335	. . . . . . . . 9
45	44	ralimi 2803	. . . . . . . 8
46		ralbi 2865	. . . . . . . 8
47	45, 46	syl 16	. . . . . . 7
48	47	exbidv 1680	. . . . . 6
49	48	adantr 465	. . . . 5 $/\$
50	49	pm5.74i 245	. . . 4 $/\$ $/\$
51	43, 50	sylibr 212	. . 3 $/\$ $/\$
52	51	alimi 1604	. 2 $/\$ $/\$
53	41, 52	impbii 188	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wal 1367

wceq 1369

wex 1586

wcel 1756

weu 2253

cab 2429

wne 2618

wral 2727

wrex 2728 $\$ cdif 3337

cin 3339

c0 3649

csn 3889

cuni 4103

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-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4415 ax-sep 4425 ax-nul 4433 ax-pr 4543 ax-un 6384

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-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2620 df-ral 2732 df-rex 2733 df-reu 2734 df-rab 2736 df-v 2986 df-sbc 3199 df-csb 3301 df-dif 3343 df-un 3345 df-in 3347 df-ss 3354 df-nul 3650 df-if 3804 df-sn 3890 df-pr 3892 df-op 3896 df-uni 4104 df-iun 4185 df-br 4305 df-opab 4363 df-mpt 4364 df-id 4648 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5393 df-fun 5432 df-fn 5433 df-f 5434 df-f1 5435 df-fo 5436 df-f1o 5437 df-fv 5438

This theorem is referenced by: dfackm 8347

W3C validator