kmlem13 - Metamath Proof Explorer

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

Theorem kmlem13 8455

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 8443	. . 3 $/\$
2		raleq 2979	. . . . . . 7
3	2	raleqbi1dv 2987	. . . . . 6
4		raleq 2979	. . . . . . 7
5	4	exbidv 1722	. . . . . 6
6	3, 5	imbi12d 318	. . . . 5
7	6	cbvalv 2030	. . . 4
8		kmlem9.1	. . . . . . 7 $\$ $\$
9	8	kmlem10 8452	. . . . . 6
10		ineq2 3608	. . . . . . . . . . . 12
11	10	eleq2d 2452	. . . . . . . . . . 11
12	11	eubidv 2240	. . . . . . . . . 10
13	12	imbi2d 314	. . . . . . . . 9
14	13	ralbidv 2821	. . . . . . . 8
15	14	cbvexv 2031	. . . . . . 7
16		kmlem3 8445	. . . . . . . . . . 11 $\$ $\$
17		ralinexa 2834	. . . . . . . . . . . 12 $/\$
18	17	rexbii 2884	. . . . . . . . . . 11 $/\$
19		rexnal 2830	. . . . . . . . . . 11 $/\$ $/\$
20	16, 18, 19	3bitri 271	. . . . . . . . . 10 $\$ $\$ $/\$
21	20	ralbii 2813	. . . . . . . . 9 $\$ $\$ $/\$
22		ralnex 2828	. . . . . . . . 9 $/\$ $/\$
23	21, 22	bitri 249	. . . . . . . 8 $\$ $\$ $/\$
24	8	kmlem12 8454	. . . . . . . . . . 11 $\$ $\$
25		vex 3037	. . . . . . . . . . . . 13
26	25	inex1 4506	. . . . . . . . . . . 12
27		ineq2 3608	. . . . . . . . . . . . . . . 16
28	27	eleq2d 2452	. . . . . . . . . . . . . . 15
29	28	eubidv 2240	. . . . . . . . . . . . . 14
30	29	imbi2d 314	. . . . . . . . . . . . 13
31	30	ralbidv 2821	. . . . . . . . . . . 12
32	26, 31	spcev 3126	. . . . . . . . . . 11
33	24, 32	syl6 33	. . . . . . . . . 10 $\$ $\$
34	33	exlimdv 1732	. . . . . . . . 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 1727	. . . 4 $/\$
40	7, 39	sylbi 195	. . 3 $/\$
41	1, 40	syl 16	. 2 $/\$ $/\$
42		kmlem7 8449	. . . . 5 $/\$ $/\$
43	42	imim1i 58	. . . 4 $/\$ $/\$
44		biimt 333	. . . . . . . . 9
45	44	ralimi 2775	. . . . . . . 8
46		ralbi 2913	. . . . . . . 8
47	45, 46	syl 16	. . . . . . 7
48	47	exbidv 1722	. . . . . 6
49	48	adantr 463	. . . . 5 $/\$
50	49	pm5.74i 245	. . . 4 $/\$ $/\$
51	43, 50	sylibr 212	. . 3 $/\$ $/\$
52	51	alimi 1641	. 2 $/\$ $/\$
53	41, 52	impbii 188	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wal 1397

wceq 1399

wex 1620

wcel 1826

weu 2218

cab 2367

wne 2577

wral 2732

wrex 2733 $\$ cdif 3386

cin 3388

c0 3711

csn 3944

cuni 4163

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504

This theorem is referenced by: dfackm 8459

W3C validator