kmlem16 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem kmlem16 4752

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4.

**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 4750	. . 3 $/\$ $/\$
5	1, 2, 3	kmlem15 4751	. . . 4 $/\$ $/\$
6	5	exbii 1047	. . 3 $/\$ $/\$
7	4, 6	orbi12i 257	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
8		19.43 1084	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
9		pm3.24 656	. . . . . 6 $/\$
10		pm3.26 319	. . . . . . . . 9 $/\$
11	10	a4s 981	. . . . . . . 8 $/\$
12	11	19.23aivv 1291	. . . . . . 7 $/\$
13		pm3.26 319	. . . . . . . . 9 $/\$
14	13	a4s 981	. . . . . . . 8 $/\$
15	14	19.23aivv 1291	. . . . . . 7 $/\$
16	12, 15	anim12i 333	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	9, 16	mto 106	. . . . 5 $/\$ $/\$ $/\$
18		19.33b 1088	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
19	17, 18	ax-mp 7	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
20	10	19.23aiv 1290	. . . . . . . . . 10 $/\$
21	13	19.23aiv 1290	. . . . . . . . . 10 $/\$
22	20, 21	anim12i 333	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
23	9, 22	mto 106	. . . . . . . 8 $/\$ $/\$ $/\$
24		19.33b 1088	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25	23, 24	ax-mp 7	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26	25	exbii 1047	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27		19.43 1084	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
28	26, 27	bitr2 174	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
29	28	albii 996	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
30	19, 29	bitr3 175	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	exbii 1047	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32	7, 8, 31	3bitr2 179	1 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 146 $\/$ wo 222 $/\$ wa 223

wal 951

wceq 953

wcel 955

wex 977

weu 1373

wne 1577

wral 1637

wrex 1638

cin 2036

This theorem is referenced by: aceqkm 4753

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-v 1803 df-in 2041