eqtfinrelk - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > eqtfinrelk		Unicode version

Theorem eqtfinrelk 4486

Description: Equality to a T raising expressed via a Kuratowski relationship. (Contributed by SF, 29-Jan-2015.)

**Hypotheses**
Ref	Expression
eqtfinrelk.1
eqtfinrelk.2

**Assertion**
Ref	Expression
eqtfinrelk	_k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin

Proof of Theorem eqtfinrelk Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4111	. . . . . . . . . 10
2	1	snid 3760	. . . . . . . . 9
3		eqtfinrelk.2	. . . . . . . . . 10
4	1, 3	opkelxpk 4248	. . . . . . . . 9 _k $/\$
5	2, 4	mpbiran 884	. . . . . . . 8 _k
6	3	elsnc 3756	. . . . . . . 8
7	5, 6	bitri 240	. . . . . . 7 _k
8	7	orbi1i 506	. . . . . 6 _k $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
9		elun 3220	. . . . . 6 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
10	1, 3	opkelxpk 4248	. . . . . . . . . . 11 _k $/\$
11	2, 3, 10	mpbir2an 886	. . . . . . . . . 10 _k
12	11	notnoti 115	. . . . . . . . 9 _k
13	12	intnan 880	. . . . . . . 8 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
14		eldif 3221	. . . . . . . 8 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
15	13, 14	mtbir 290	. . . . . . 7 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
16	15	biorfi 396	. . . . . 6 $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
17	8, 9, 16	3bitr4i 268	. . . . 5 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
18	17	a1i 10	. . . 4 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
19		sneq 3744	. . . . . 6
20	19	opkeq1d 4065	. . . . 5
21	20	eleq1d 2419	. . . 4 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
22		iftrue 3668	. . . . 5 Nn $/\$ ₁
23	22	eqeq2d 2364	. . . 4 Nn $/\$ ₁
24	18, 21, 23	3bitr4d 276	. . 3 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Nn $/\$ ₁
25		iffalse 3669	. . . . 5 Nn $/\$ ₁ Nn $/\$ ₁
26	25	eqeq2d 2364	. . . 4 Nn $/\$ ₁ Nn $/\$ ₁
27		opkex 4113	. . . . . . . . 9
28	27	elimak 4259	. . . . . . . 8 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
29		elpw121c 4148	. . . . . . . . . . . 12 ₁ ₁ 1_c
30	29	anbi1i 676	. . . . . . . . . . 11 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
31		19.41v 1901	. . . . . . . . . . 11 $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
32	30, 31	bitr4i 243	. . . . . . . . . 10 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
33	32	exbii 1582	. . . . . . . . 9 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
34		df-rex 2620	. . . . . . . . 9 ₁ ₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
35		excom 1741	. . . . . . . . 9 $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
36	33, 34, 35	3bitr4i 268	. . . . . . . 8 ₁ ₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
37		snex 4111	. . . . . . . . . . 11
38		opkeq1 4059	. . . . . . . . . . . 12
39	38	eleq1d 2419	. . . . . . . . . . 11 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
40	37, 39	ceqsexv 2894	. . . . . . . . . 10 $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
41		elsymdif 3223	. . . . . . . . . . 11 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
42		snex 4111	. . . . . . . . . . . . . 14
43		snex 4111	. . . . . . . . . . . . . 14
44	42, 43, 3	otkelins2k 4255	. . . . . . . . . . . . 13 Ins2_k S_k S_k
45		vex 2862	. . . . . . . . . . . . . 14
46	45, 3	elssetk 4270	. . . . . . . . . . . . 13 S_k
47	44, 46	bitri 240	. . . . . . . . . . . 12 Ins2_k S_k
48		snex 4111	. . . . . . . . . . . . . . . 16
49		opkeq1 4059	. . . . . . . . . . . . . . . . 17
50	49	eleq1d 2419	. . . . . . . . . . . . . . . 16 Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
51	48, 50	ceqsexv 2894	. . . . . . . . . . . . . . 15 $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
52		eldif 3221	. . . . . . . . . . . . . . 15 Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c Ins3_k _k S_k $/\$ Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
53		vex 2862	. . . . . . . . . . . . . . . . . 18
54	53, 42, 43	otkelins3k 4256	. . . . . . . . . . . . . . . . 17 Ins3_k _k S_k _k S_k
55	53, 42	opkelcnvk 4250	. . . . . . . . . . . . . . . . 17 _k S_k S_k
56	45, 53	elssetk 4270	. . . . . . . . . . . . . . . . 17 S_k
57	54, 55, 56	3bitri 262	. . . . . . . . . . . . . . . 16 Ins3_k _k S_k
58	53, 42, 43	otkelins2k 4255	. . . . . . . . . . . . . . . . . 18 Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
59		opkex 4113	. . . . . . . . . . . . . . . . . . . 20
60	59	elimak 4259	. . . . . . . . . . . . . . . . . . 19 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c ₁ 1_c Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
61		elpw11c 4147	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ 1_c
62	61	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . 22 ₁ 1_c $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
63		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
64	62, 63	bitr4i 243	. . . . . . . . . . . . . . . . . . . . 21 ₁ 1_c $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
65	64	exbii 1582	. . . . . . . . . . . . . . . . . . . 20 ₁ 1_c $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
66		df-rex 2620	. . . . . . . . . . . . . . . . . . . 20 ₁ 1_c Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k ₁ 1_c $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
67		excom 1741	. . . . . . . . . . . . . . . . . . . 20 $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
68	65, 66, 67	3bitr4i 268	. . . . . . . . . . . . . . . . . . 19 ₁ 1_c Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
69		snex 4111	. . . . . . . . . . . . . . . . . . . . . 22
70		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . 23
71	70	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
72	69, 71	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
73		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k
74		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . 25
75	74, 53, 43	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
76		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . 24 Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn _k $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
77	74, 43	opkelxpk 4248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn _k Nn $/\$
78	43, 77	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . . . . 25 Nn _k Nn
79		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
80		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
81	80	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
82	79, 81	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
83		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k SI_k S_k $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
84		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	84, 74, 43	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2_k SI_k S_k SI_k S_k
86		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
87		eqtfinrelk.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
88	86, 87	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SI_k S_k S_k
89		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
90	89, 87	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 S_k
91	85, 88, 90	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k SI_k S_k
92		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	92	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
94		elpw121c 4148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ₁ ₁ 1_c
95	94	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
96		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
97	95, 96	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
98	97	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
99		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
100		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
101	98, 99, 100	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
102		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
103		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
104	103	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
105	102, 104	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
106		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins2_k S_k
107		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
108	107, 84, 74	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c
109		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
110	109, 86	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c
111	109, 89	eqpw1relk 4479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
112	108, 110, 111	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
113	107, 84, 74	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2_k S_k S_k
114	109, 74	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 S_k
115	113, 114	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2_k S_k
116	112, 115	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins2_k S_k ₁ $/\$
117	105, 106, 116	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k ₁ $/\$
118	117	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k ₁ $/\$
119	93, 101, 118	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ $/\$
120	84, 74, 43	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
121		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ₁ ₁ $/\$
122	119, 120, 121	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁
123	91, 122	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2_k SI_k S_k $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ ₁
124	82, 83, 123	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ ₁
125	124	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ ₁
126		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
127		elpw131c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ₁ ₁ ₁ 1_c
128	127	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
129		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
130	128, 129	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
131	130	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
132	126, 131	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
133		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	133	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
135		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
136	132, 134, 135	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
137		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ $/\$ ₁
138	125, 136, 137	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁
139	78, 138	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 Nn _k $/\$ Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ₁
140	75, 76, 139	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ₁
141	74, 53, 43	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k _k _k
142		opkelidkg 4274	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ _k
143	74, 53, 142	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . 24 _k
144	141, 143	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k _k
145	140, 144	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Nn $/\$ ₁
146	73, 145	xchbinx 301	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Nn $/\$ ₁
147	72, 146	bitri 240	. . . . . . . . . . . . . . . . . . . 20 $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Nn $/\$ ₁
148	147	exbii 1582	. . . . . . . . . . . . . . . . . . 19 $/\$ Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k Nn $/\$ ₁
149	60, 68, 148	3bitri 262	. . . . . . . . . . . . . . . . . 18 Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c Nn $/\$ ₁
150		exnal 1574	. . . . . . . . . . . . . . . . . 18 Nn $/\$ ₁ Nn $/\$ ₁
151	58, 149, 150	3bitrri 263	. . . . . . . . . . . . . . . . 17 Nn $/\$ ₁ Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
152	151	con1bii 321	. . . . . . . . . . . . . . . 16 Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c Nn $/\$ ₁
153	57, 152	anbi12i 678	. . . . . . . . . . . . . . 15 Ins3_k _k S_k $/\$ Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Nn $/\$ ₁
154	51, 52, 153	3bitri 262	. . . . . . . . . . . . . 14 $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Nn $/\$ ₁
155	154	exbii 1582	. . . . . . . . . . . . 13 $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Nn $/\$ ₁
156	42, 43, 3	otkelins3k 4256	. . . . . . . . . . . . . 14 Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c
157		opkex 4113	. . . . . . . . . . . . . . 15
158	157	elimak 4259	. . . . . . . . . . . . . 14 Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c ₁ 1_c Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
159		elpw11c 4147	. . . . . . . . . . . . . . . . . 18 ₁ 1_c
160	159	anbi1i 676	. . . . . . . . . . . . . . . . 17 ₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
161		19.41v 1901	. . . . . . . . . . . . . . . . 17 $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
162	160, 161	bitr4i 243	. . . . . . . . . . . . . . . 16 ₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
163	162	exbii 1582	. . . . . . . . . . . . . . 15 ₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
164		df-rex 2620	. . . . . . . . . . . . . . 15 ₁ 1_c Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c ₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
165		excom 1741	. . . . . . . . . . . . . . 15 $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
166	163, 164, 165	3bitr4i 268	. . . . . . . . . . . . . 14 ₁ 1_c Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
167	156, 158, 166	3bitri 262	. . . . . . . . . . . . 13 Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c $/\$ Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c
168		dfiota2 4340	. . . . . . . . . . . . . . 15 Nn $/\$ ₁ Nn $/\$ ₁
169	168	eleq2i 2417	. . . . . . . . . . . . . 14 Nn $/\$ ₁ Nn $/\$ ₁
170		eluniab 3903	. . . . . . . . . . . . . 14 Nn $/\$ ₁ $/\$ Nn $/\$ ₁
171	169, 170	bitri 240	. . . . . . . . . . . . 13 Nn $/\$ ₁ $/\$ Nn $/\$ ₁
172	155, 167, 171	3bitr4i 268	. . . . . . . . . . . 12 Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Nn $/\$ ₁
173	47, 172	bibi12i 306	. . . . . . . . . . 11 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Nn $/\$ ₁
174	41, 173	xchbinx 301	. . . . . . . . . 10 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Nn $/\$ ₁
175	40, 174	bitri 240	. . . . . . . . 9 $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Nn $/\$ ₁
176	175	exbii 1582	. . . . . . . 8 $/\$ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c Nn $/\$ ₁
177	28, 36, 176	3bitri 262	. . . . . . 7 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c Nn $/\$ ₁
178	177	notbii 287	. . . . . 6 Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c Nn $/\$ ₁
179	27	elcompl 3225	. . . . . 6 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c
180		dfcleq 2347	. . . . . . 7 Nn $/\$ ₁ Nn $/\$ ₁
181		alex 1572	. . . . . . 7 Nn $/\$ ₁ Nn $/\$ ₁
182	180, 181	bitri 240	. . . . . 6 Nn $/\$ ₁ Nn $/\$ ₁
183	178, 179, 182	3bitr4i 268	. . . . 5 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c Nn $/\$ ₁
184	183	a1i 10	. . . 4 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c Nn $/\$ ₁
185	43, 3	opkelxpk 4248	. . . . . . . . . . 11 _k $/\$
186	3	biantru 491	. . . . . . . . . . 11 $/\$
187	43	elsnc 3756	. . . . . . . . . . . 12
188	87	sneqb 3876	. . . . . . . . . . . 12
189	187, 188	bitri 240	. . . . . . . . . . 11
190	185, 186, 189	3bitr2i 264	. . . . . . . . . 10 _k
191	190	biimpi 186	. . . . . . . . 9 _k
192	191	con3i 127	. . . . . . . 8 _k
193	192	biantrud 493	. . . . . . 7 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
194		simpl 443	. . . . . . . . 9 $/\$
195	194	con3i 127	. . . . . . . 8 $/\$
196		biorf 394	. . . . . . . 8 $/\$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k $/\$ $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
197	195, 196	syl 15	. . . . . . 7 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k $/\$ $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
198	193, 197	bitrd 244	. . . . . 6 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
199	43, 3	opkelxpk 4248	. . . . . . . 8 _k $/\$
200	189, 6	anbi12i 678	. . . . . . . 8 $/\$ $/\$
201	199, 200	bitri 240	. . . . . . 7 _k $/\$
202		eldif 3221	. . . . . . 7 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
203	201, 202	orbi12i 507	. . . . . 6 _k $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $/\$ $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c $/\$ _k
204	198, 203	syl6bbr 254	. . . . 5 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
205		elun 3220	. . . . 5 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k $\/$ ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
206	204, 205	syl6bbr 254	. . . 4 ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
207	26, 184, 206	3bitr2rd 273	. . 3 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Nn $/\$ ₁
208	24, 207	pm2.61i 156	. 2 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Nn $/\$ ₁
209		df-tfin 4443	. . 3 T_fin Nn $/\$ ₁
210	209	eqeq2i 2363	. 2 T_fin Nn $/\$ ₁
211	208, 210	bitr4i 243	1 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176 $\/$ wo 357 $/\$ wa 358

wal 1540

wex 1541

wceq 1642

wcel 1710

cab 2339

wrex 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cun 3207

cin 3208

csymdif 3209

c0 3550

cif 3662

cpw 3722

csn 3737

cuni 3891

copk 4057 1_cc1c 4134

₁ cpw1 4135

_k cxpk 4174

_kccnvk 4175 Ins2_k cins2k 4176 Ins3_k cins3k 4177

_kcimak 4179 SI_k csik 4181 S_k cssetk 4183

_k cidk 4184

cio 4337 Nn cnnc 4373 T_fin ctfin 4435

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-sn 4087

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-opk 4058 df-1c 4136 df-pw1 4137 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-sik 4192 df-ssetk 4193 df-idk 4195 df-iota 4339 df-tfin 4443

This theorem is referenced by: sfintfinlem1 4531 tfinnnlem1 4533 vfinspss 4551 vfinspclt 4552 vfinncsp 4554

W3C validator