kmlem13 - Metamath Proof Explorer

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

Theorem kmlem13 8554

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 8542	. . 3 $/\$
2		raleq 3063	. . . . . . 7
3	2	raleqbi1dv 3071	. . . . . 6
4		raleq 3063	. . . . . . 7
5	4	exbidv 1690	. . . . . 6
6	3, 5	imbi12d 320	. . . . 5
7	6	cbvalv 1996	. . . 4
8		kmlem9.1	. . . . . . 7 $\$ $\$
9	8	kmlem10 8551	. . . . . 6
10		ineq2 3699	. . . . . . . . . . . 12
11	10	eleq2d 2537	. . . . . . . . . . 11
12	11	eubidv 2298	. . . . . . . . . 10
13	12	imbi2d 316	. . . . . . . . 9
14	13	ralbidv 2906	. . . . . . . 8
15	14	cbvexv 1997	. . . . . . 7
16		kmlem3 8544	. . . . . . . . . . 11 $\$ $\$
17		ralinexa 2919	. . . . . . . . . . . 12 $/\$
18	17	rexbii 2969	. . . . . . . . . . 11 $/\$
19		rexnal 2915	. . . . . . . . . . 11 $/\$ $/\$
20	16, 18, 19	3bitri 271	. . . . . . . . . 10 $\$ $\$ $/\$
21	20	ralbii 2898	. . . . . . . . 9 $\$ $\$ $/\$
22		ralnex 2913	. . . . . . . . 9 $/\$ $/\$
23	21, 22	bitri 249	. . . . . . . 8 $\$ $\$ $/\$
24	8	kmlem12 8553	. . . . . . . . . . 11 $\$ $\$
25		vex 3121	. . . . . . . . . . . . 13
26	25	inex1 4594	. . . . . . . . . . . 12
27		ineq2 3699	. . . . . . . . . . . . . . . 16
28	27	eleq2d 2537	. . . . . . . . . . . . . . 15
29	28	eubidv 2298	. . . . . . . . . . . . . 14
30	29	imbi2d 316	. . . . . . . . . . . . 13
31	30	ralbidv 2906	. . . . . . . . . . . 12
32	26, 31	spcev 3210	. . . . . . . . . . 11
33	24, 32	syl6 33	. . . . . . . . . 10 $\$ $\$
34	33	exlimdv 1700	. . . . . . . . 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 1695	. . . 4 $/\$
40	7, 39	sylbi 195	. . 3 $/\$
41	1, 40	syl 16	. 2 $/\$ $/\$
42		kmlem7 8548	. . . . 5 $/\$ $/\$
43	42	imim1i 58	. . . 4 $/\$ $/\$
44		biimt 335	. . . . . . . . 9
45	44	ralimi 2860	. . . . . . . 8
46		ralbi 2998	. . . . . . . 8
47	45, 46	syl 16	. . . . . . 7
48	47	exbidv 1690	. . . . . 6
49	48	adantr 465	. . . . 5 $/\$
50	49	pm5.74i 245	. . . 4 $/\$ $/\$
51	43, 50	sylibr 212	. . 3 $/\$ $/\$
52	51	alimi 1614	. 2 $/\$ $/\$
53	41, 52	impbii 188	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wal 1377

wceq 1379

wex 1596

wcel 1767

weu 2275

cab 2452

wne 2662

wral 2817

wrex 2818 $\$ cdif 3478

cin 3480

c0 3790

csn 4033

cuni 4251

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-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4564 ax-sep 4574 ax-nul 4582 ax-pr 4692 ax-un 6587

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-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2822 df-rex 2823 df-reu 2824 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-nul 3791 df-if 3946 df-sn 4034 df-pr 4036 df-op 4040 df-uni 4252 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-id 4801 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602

This theorem is referenced by: dfackm 8558

W3C validator