kmlem16 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem kmlem16 4763

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 4761	. . 3 $/\$ $/\$
5	1, 2, 3	kmlem15 4762	. . . 4 $/\$ $/\$
6	5	exbii 1050	. . 3 $/\$ $/\$
7	4, 6	orbi12i 257	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
8		19.43 1087	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
9		pm3.24 657	. . . . . 6 $/\$
10		pm3.26 319	. . . . . . . . 9 $/\$
11	10	a4s 983	. . . . . . . 8 $/\$
12	11	19.23aivv 1295	. . . . . . 7 $/\$
13		pm3.26 319	. . . . . . . . 9 $/\$
14	13	a4s 983	. . . . . . . 8 $/\$
15	14	19.23aivv 1295	. . . . . . 7 $/\$
16	12, 15	anim12i 333	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	9, 16	mto 106	. . . . 5 $/\$ $/\$ $/\$
18		19.33b 1091	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
19	17, 18	ax-mp 7	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
20	10	19.23aiv 1294	. . . . . . . . . 10 $/\$
21	13	19.23aiv 1294	. . . . . . . . . 10 $/\$
22	20, 21	anim12i 333	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
23	9, 22	mto 106	. . . . . . . 8 $/\$ $/\$ $/\$
24		19.33b 1091	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25	23, 24	ax-mp 7	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26	25	exbii 1050	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27		19.43 1087	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
28	26, 27	bitr2 174	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
29	28	albii 998	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
30	19, 29	bitr3 175	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	exbii 1050	. 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 953

wceq 955

wcel 957

wex 979

weu 1379

wne 1583

wral 1643

wrex 1644

cin 2043

This theorem is referenced by: aceqkm 4764

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 961 ax-gen 962 ax-8 963 ax-10 965 ax-11 966 ax-12 967 ax-17 970 ax-4 972 ax-5o 974 ax-6o 977 ax-9o 1122 ax-10o 1139 ax-16 1209 ax-11o 1217 ax-ext 1458

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 980 df-sb 1171 df-eu 1381 df-clab 1463 df-cleq 1468 df-clel 1471 df-ne 1585 df-ral 1647 df-rex 1648 df-v 1809 df-in 2048