kmlem16 - Metamath Proof Explorer

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

Theorem kmlem16 8987

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

**Assertion**
Ref	Expression
kmlem16	$/\$ $\/$ $/\$ $/\$ $\/$ $/\$

(

)

(

)

(

)

**Proof of Theorem kmlem16**
Step	Hyp	Ref	Expression
1		kmlem14.1	. . . 4 $/\$ $/\$
2		kmlem14.2	. . . 4 $/\$ $/\$ $/\$
3		kmlem14.3	. . . 4
4	1, 2, 3	kmlem14 8985	. . 3 $/\$ $/\$
5	1, 2, 3	kmlem15 8986	. . . 4 $/\$ $/\$
6	5	exbii 1774	. . 3 $/\$ $/\$
7	4, 6	orbi12i 543	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
8		19.43 1810	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
9		pm3.24 926	. . . . . 6 $/\$
10		simpl 473	. . . . . . . . 9 $/\$
11	10	sps 2055	. . . . . . . 8 $/\$
12	11	exlimivv 1860	. . . . . . 7 $/\$
13		simpl 473	. . . . . . . . 9 $/\$
14	13	sps 2055	. . . . . . . 8 $/\$
15	14	exlimivv 1860	. . . . . . 7 $/\$
16	12, 15	anim12i 590	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	9, 16	mto 188	. . . . 5 $/\$ $/\$ $/\$
18		19.33b 1813	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
19	17, 18	ax-mp 5	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
20	10	exlimiv 1858	. . . . . . . . . 10 $/\$
21	13	exlimiv 1858	. . . . . . . . . 10 $/\$
22	20, 21	anim12i 590	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
23	9, 22	mto 188	. . . . . . . 8 $/\$ $/\$ $/\$
24		19.33b 1813	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25	23, 24	ax-mp 5	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26	25	exbii 1774	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27		19.43 1810	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
28	26, 27	bitr2i 265	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
29	28	albii 1747	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
30	19, 29	bitr3i 266	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	exbii 1774	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32	7, 8, 31	3bitr2i 288	1 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wal 1481

wex 1704

wcel 1990

weu 2470

wne 2794

wral 2912

wrex 2913

cin 3573

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-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-v 3202 df-in 3581

This theorem is referenced by: dfackm 8988