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 8597

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 8585	. . 3 $/\$
2		raleq 2989	. . . . . . 7
3	2	raleqbi1dv 2997	. . . . . 6
4		raleq 2989	. . . . . . 7
5	4	exbidv 1770	. . . . . 6
6	3, 5	imbi12d 322	. . . . 5
7	6	cbvalv 2118	. . . 4
8		kmlem9.1	. . . . . . 7 $\$ $\$
9	8	kmlem10 8594	. . . . . 6
10		ineq2 3630	. . . . . . . . . . . 12
11	10	eleq2d 2516	. . . . . . . . . . 11
12	11	eubidv 2321	. . . . . . . . . 10
13	12	imbi2d 318	. . . . . . . . 9
14	13	ralbidv 2829	. . . . . . . 8
15	14	cbvexv 2119	. . . . . . 7
16		kmlem3 8587	. . . . . . . . . . 11 $\$ $\$
17		ralinexa 2841	. . . . . . . . . . . 12 $/\$
18	17	rexbii 2891	. . . . . . . . . . 11 $/\$
19		rexnal 2838	. . . . . . . . . . 11 $/\$ $/\$
20	16, 18, 19	3bitri 275	. . . . . . . . . 10 $\$ $\$ $/\$
21	20	ralbii 2821	. . . . . . . . 9 $\$ $\$ $/\$
22		ralnex 2836	. . . . . . . . 9 $/\$ $/\$
23	21, 22	bitri 253	. . . . . . . 8 $\$ $\$ $/\$
24	8	kmlem12 8596	. . . . . . . . . . 11 $\$ $\$
25		vex 3050	. . . . . . . . . . . . 13
26	25	inex1 4547	. . . . . . . . . . . 12
27		ineq2 3630	. . . . . . . . . . . . . . . 16
28	27	eleq2d 2516	. . . . . . . . . . . . . . 15
29	28	eubidv 2321	. . . . . . . . . . . . . 14
30	29	imbi2d 318	. . . . . . . . . . . . 13
31	30	ralbidv 2829	. . . . . . . . . . . 12
32	26, 31	spcev 3143	. . . . . . . . . . 11
33	24, 32	syl6 34	. . . . . . . . . 10 $\$ $\$
34	33	exlimdv 1781	. . . . . . . . 9 $\$ $\$
35	34	com12 32	. . . . . . . 8 $\$ $\$
36	23, 35	syl5bir 222	. . . . . . 7 $/\$
37	15, 36	sylbi 199	. . . . . 6 $/\$
38	9, 37	syl 17	. . . . 5 $/\$
39	38	alrimiv 1775	. . . 4 $/\$
40	7, 39	sylbi 199	. . 3 $/\$
41	1, 40	syl 17	. 2 $/\$ $/\$
42		kmlem7 8591	. . . . 5 $/\$ $/\$
43	42	imim1i 60	. . . 4 $/\$ $/\$
44		biimt 337	. . . . . . . . 9
45	44	ralimi 2783	. . . . . . . 8
46		ralbi 2923	. . . . . . . 8
47	45, 46	syl 17	. . . . . . 7
48	47	exbidv 1770	. . . . . 6
49	48	adantr 467	. . . . 5 $/\$
50	49	pm5.74i 249	. . . 4 $/\$ $/\$
51	43, 50	sylibr 216	. . 3 $/\$ $/\$
52	51	alimi 1686	. 2 $/\$ $/\$
53	41, 52	impbii 191	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wal 1444

wceq 1446

wex 1665

wcel 1889

weu 2301

cab 2439

wne 2624

wral 2739

wrex 2740 $\$ cdif 3403

cin 3405

c0 3733

csn 3970

cuni 4201

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-reu 2746 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593

This theorem is referenced by: dfackm 8601

W3C validator