Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem kmlem16 3595

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

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

Distinct variable group(s):

**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 3593	. . 3 $/\$ $/\$
5	1, 2, 3	kmlem15 3594	. . . 4 $/\$ $/\$
6	5	biex 733	. . 3 $/\$ $/\$
7	4, 6	orbi12i 216	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
8		19.43 767	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
9		pm3.24 496	. . . . . . 7 $/\$
10		pm3.26 256	. . . . . . . . . 10 $/\$
11	10	a4s 682	. . . . . . . . 9 $/\$
12	11	19.23aivv 953	. . . . . . . 8 $/\$
13		pm3.26 256	. . . . . . . . . 10 $/\$
14	13	a4s 682	. . . . . . . . 9 $/\$
15	14	19.23aivv 953	. . . . . . . 8 $/\$
16	12, 15	anim12i 268	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
17	9, 16	mto 93	. . . . . 6 $/\$ $/\$ $/\$
18		19.33b 771	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
19	17, 18	ax-mp 6	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
20	10	19.23aiv 952	. . . . . . . . . . 11 $/\$
21	13	19.23aiv 952	. . . . . . . . . . 11 $/\$
22	20, 21	anim12i 268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	9, 22	mto 93	. . . . . . . . 9 $/\$ $/\$ $/\$
24		19.33b 771	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25	23, 24	ax-mp 6	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26	25	biex 733	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27		19.43 767	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
28	26, 27	bitr2 152	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
29	28	bial 695	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
30	19, 29	bitr3 153	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	biex 733	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32	8, 31	bitr3 153	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	7, 32	bitr 151	1 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 1

wi 2

wb 127 $\/$ wo 195 $/\$ wa 196

wal 672

wex 678

weq 797

wel 803

weu 1007

wcel 1092

wral 1201

wrex 1202

cin 1486

This theorem is referenced by: aceqkm 3596

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-16 922 ax-17 925 ax-ext 1074

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-ex 679 df-sb 853 df-eu 1009 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-in 1491