kmlem16 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem kmlem16 5942

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 5940	. . 3 $/\$ $/\$
5	1, 2, 3	kmlem15 5941	. . . 4 $/\$ $/\$
6	5	exbii 1398	. . 3 $/\$ $/\$
7	4, 6	orbi12i 277	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
8		19.43 1440	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
9		pm3.24 720	. . . . . 6 $/\$
10		simpl 346	. . . . . . . . 9 $/\$
11	10	a4s 1330	. . . . . . . 8 $/\$
12	11	19.23aivv 1675	. . . . . . 7 $/\$
13		simpl 346	. . . . . . . . 9 $/\$
14	13	a4s 1330	. . . . . . . 8 $/\$
15	14	19.23aivv 1675	. . . . . . 7 $/\$
16	12, 15	anim12i 360	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	9, 16	mto 121	. . . . 5 $/\$ $/\$ $/\$
18		19.33b 1444	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
19	17, 18	ax-mp 7	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
20	10	19.23aiv 1674	. . . . . . . . . 10 $/\$
21	13	19.23aiv 1674	. . . . . . . . . 10 $/\$
22	20, 21	anim12i 360	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
23	9, 22	mto 121	. . . . . . . 8 $/\$ $/\$ $/\$
24		19.33b 1444	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25	23, 24	ax-mp 7	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26	25	exbii 1398	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27		19.43 1440	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
28	26, 27	bitr2i 191	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
29	28	albii 1346	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
30	19, 29	bitr3i 192	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	exbii 1398	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32	7, 8, 31	3bitr2i 196	1 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240

wal 1296

wceq 1298

wcel 1300

wex 1326

weu 1771

wne 2017

wral 2105

wrex 2106

cin 2592

This theorem is referenced by: aceqkm 5943

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-v 2294 df-in 2603