ltfinex - New Foundations Explorer

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

Theorem ltfinex 4464

Description: Finite less than is stratified. (Contributed by SF, 29-Jan-2015.)

**Assertion**
Ref	Expression
ltfinex	_fin

Proof of Theorem ltfinex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ltfin 4441	. . 3 _fin $/\$ $/\$ Nn 1_c
2		elin 3219	. . . . 5 _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k _k $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
3		elvvk 4207	. . . . . 6 _k
4	3	anbi1i 676	. . . . 5 _k $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
5		19.41vv 1902	. . . . . 6 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
6		eleq1 2413	. . . . . . . . 9 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
7		opkex 4113	. . . . . . . . . . . . 13
8	7	elimak 4259	. . . . . . . . . . . 12 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn ₁ ₁ Nn ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
9		elpw12 4145	. . . . . . . . . . . . . . . 16 ₁ ₁ Nn Nn
10	9	anbi1i 676	. . . . . . . . . . . . . . 15 ₁ ₁ Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
11		r19.41v 2764	. . . . . . . . . . . . . . 15 Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
12	10, 11	bitr4i 243	. . . . . . . . . . . . . 14 ₁ ₁ Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
13	12	exbii 1582	. . . . . . . . . . . . 13 ₁ ₁ Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
14		df-rex 2620	. . . . . . . . . . . . 13 ₁ ₁ Nn ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁ ₁ Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
15		rexcom4 2878	. . . . . . . . . . . . 13 Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
16	13, 14, 15	3bitr4i 268	. . . . . . . . . . . 12 ₁ ₁ Nn ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
17		snex 4111	. . . . . . . . . . . . . . 15
18		opkeq1 4059	. . . . . . . . . . . . . . . 16
19	18	eleq1d 2419	. . . . . . . . . . . . . . 15 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
20	17, 19	ceqsexv 2894	. . . . . . . . . . . . . 14 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
21		opkex 4113	. . . . . . . . . . . . . . . 16
22	21	elimak 4259	. . . . . . . . . . . . . . 15 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁ ₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
23		elpw131c 4149	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ ₁ 1_c
24	23	anbi1i 676	. . . . . . . . . . . . . . . . . 18 ₁ ₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
25		19.41v 1901	. . . . . . . . . . . . . . . . . 18 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
26	24, 25	bitr4i 243	. . . . . . . . . . . . . . . . 17 ₁ ₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
27	26	exbii 1582	. . . . . . . . . . . . . . . 16 ₁ ₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
28		df-rex 2620	. . . . . . . . . . . . . . . 16 ₁ ₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c ₁ ₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
29		excom 1741	. . . . . . . . . . . . . . . 16 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
30	27, 28, 29	3bitr4i 268	. . . . . . . . . . . . . . 15 ₁ ₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
31		snex 4111	. . . . . . . . . . . . . . . . . 18
32		opkeq1 4059	. . . . . . . . . . . . . . . . . . 19
33	32	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
34	31, 33	ceqsexv 2894	. . . . . . . . . . . . . . . . 17 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
35		elin 3219	. . . . . . . . . . . . . . . . 17 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
36		opkex 4113	. . . . . . . . . . . . . . . . . . . . . 22
37	36	elimak 4259	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
38		elpw161c 4152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ ₁ ₁ ₁ ₁ 1_c
39	38	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . 24 ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
40		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
41	39, 40	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
42	41	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
43		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
44		excom 1741	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
45	42, 43, 44	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
46		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . 24
47		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . 25
48	47	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
49	46, 48	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
50		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
51		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
52	51, 31, 21	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k S_k
53		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
55	53, 54	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k S_k
56		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
57		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58	56, 57	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 SI_k SI_k SI_k S_k SI_k SI_k S_k
59		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
60		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
61	59, 60	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 SI_k SI_k S_k SI_k S_k
62		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
63		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	62, 63	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI_k S_k S_k
65		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
66	65, 63	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 S_k
67	64, 66	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 SI_k S_k
68	58, 61, 67	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 SI_k SI_k SI_k S_k
69	52, 55, 68	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3_k SI_k SI_k SI_k SI_k S_k
70		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
71	70	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
72		elpw161c 4152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ₁ ₁ ₁ ₁ ₁ ₁ 1_c
73	72	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
74		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
75	73, 74	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
76	75	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
77		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
78		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
79	76, 77, 78	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
80		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
81		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
82	81	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
83	80, 82	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
84		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
85		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
86	85, 51, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins2_k Ins3_k SI_k SI_k S_k Ins3_k SI_k SI_k S_k
87		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
88	87, 17, 7	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3_k SI_k SI_k S_k SI_k SI_k S_k
89		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
90		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
91	89, 90	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 SI_k SI_k S_k SI_k S_k
92		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
93		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
94	92, 93	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 SI_k S_k S_k
95		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
96	95, 93	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 S_k
97	91, 94, 96	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SI_k SI_k S_k
98	86, 88, 97	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2_k Ins3_k SI_k SI_k S_k
99		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100	99	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
101		elpw181c 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
102	101	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
103		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
104	102, 103	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
105	104	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
106		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
107		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
108	105, 106, 107	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
109		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
110		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
111	110	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
112	109, 111	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
113		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins2_k Ins3_k S_k $/\$ Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
114		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
115	114, 80, 70	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins2_k Ins2_k Ins3_k S_k
116		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
117	116, 51, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2_k Ins2_k Ins3_k S_k Ins2_k Ins3_k S_k
118		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
119	118, 17, 7	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2_k Ins3_k S_k Ins3_k S_k
120		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
121		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
122		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
123	120, 121, 122	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3_k S_k S_k
124		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
125	124, 121	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 S_k
126	119, 123, 125	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2_k Ins3_k S_k
127	115, 117, 126	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2_k Ins2_k Ins2_k Ins3_k S_k
128		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c $/\$ ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
129	114, 80, 70	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
130		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
131		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
132	130, 131	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
133	116, 85	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
134		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
135		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
136	134, 135	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
137	118, 87	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
138		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
139	138, 89	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
140	120, 92	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
141	124, 95	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
142	124, 95	ndisjrelk 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
143	142	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
144		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
145	144	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
146		df-ne 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
147	146	con2bii 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
148	143, 145, 147	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
149	140, 141, 148	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
150	137, 139, 149	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
151	133, 136, 150	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
152	129, 132, 151	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
153		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
154	153	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
155		elpw1111c 4157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
156	155	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
157		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
158	156, 157	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
159	158	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
160		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
161		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
162	159, 160, 161	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
163		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
164		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
165	164	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
166	163, 165	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
167		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
168		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
169	168, 109, 99	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
170		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
171	170, 80, 70	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
172		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
173	172, 51, 21	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins3_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k S_k
174		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
175	174, 53	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k S_k
176		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
177	176, 56	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k S_k
178		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
179	178, 59	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SI_k SI_k SI_k S_k SI_k SI_k S_k
180		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
181	180, 62	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k S_k SI_k S_k
182		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
183	182, 65	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k S_k S_k
184		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
185	184, 65	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 S_k
186	181, 183, 185	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SI_k SI_k S_k
187	177, 179, 186	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 SI_k SI_k SI_k SI_k S_k
188	173, 175, 187	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
189	169, 171, 188	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
190	168, 109, 99	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
191		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
192		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
193	191, 192	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
194	170, 114	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
195		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
196	195, 130	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
197	172, 116	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k S_k
198	174, 134	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k S_k
199	176, 118	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k S_k
200	178, 138	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 SI_k SI_k SI_k S_k SI_k SI_k S_k
201	180, 120	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 SI_k SI_k S_k SI_k S_k
202	182, 124	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 SI_k S_k S_k
203	184, 124	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 S_k
204	201, 202, 203	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 SI_k SI_k S_k
205	199, 200, 204	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SI_k SI_k SI_k SI_k S_k
206	197, 198, 205	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k SI_k SI_k SI_k SI_k S_k
207	194, 196, 206	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
208	190, 193, 207	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
209	168, 109, 99	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
210	170, 80, 70	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
211	195, 131	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
212	172, 85	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k SI_k S_k
213	174, 135	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SI_k SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k SI_k S_k
214	176, 87	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SI_k SI_k SI_k SI_k S_k SI_k SI_k SI_k S_k
215	178, 89	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 SI_k SI_k SI_k S_k SI_k SI_k S_k
216	180, 92	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 SI_k SI_k S_k SI_k S_k
217	182, 95	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 SI_k S_k S_k
218	184, 95	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 S_k
219	217, 218	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 SI_k S_k
220	215, 216, 219	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SI_k SI_k SI_k S_k
221	213, 214, 220	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SI_k SI_k SI_k SI_k SI_k S_k
222	211, 212, 221	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
223	209, 210, 222	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
224	208, 223	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $\/$ Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $\/$
225		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k $\/$ Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
226		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $\/$
227	224, 225, 226	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
228	189, 227	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
229	228	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
230	166, 167, 229	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
231	230	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
232	154, 162, 231	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
233	232	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
234	153	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
235		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
236		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
237	235, 236	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
238	233, 234, 237	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
239	152, 238	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c $/\$ ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
240	128, 239	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
241	127, 240	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2_k Ins2_k Ins2_k Ins3_k S_k $/\$ Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
242	112, 113, 241	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
243	242	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
244	100, 108, 243	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
245		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
246	244, 245	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
247	98, 246	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k Ins3_k SI_k SI_k S_k $/\$ Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
248	83, 84, 247	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
249	248	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
250	71, 79, 249	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ $/\$
251	51, 31, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
252		rexcom 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
253		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
254	252, 253	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
255	250, 251, 254	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
256	69, 255	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
257	256	notbii 287	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
258	49, 50, 257	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
259	258	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
260	37, 45, 259	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
261	260	notbii 287	. . . . . . . . . . . . . . . . . . 19 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$
262	36	elcompl 3225	. . . . . . . . . . . . . . . . . . 19 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
263		df-addc 4378	. . . . . . . . . . . . . . . . . . . . 21 $/\$
264	263	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . 20 $/\$
265		abeq2 2458	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
266		alex 1572	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
267	264, 265, 266	3bitri 262	. . . . . . . . . . . . . . . . . . 19 $/\$
268	261, 262, 267	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
269	57, 17, 7	otkelins2k 4255	. . . . . . . . . . . . . . . . . . 19 Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
270	63, 121, 122	otkelins2k 4255	. . . . . . . . . . . . . . . . . . 19 Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
271	63, 122	opkelimagek 4272	. . . . . . . . . . . . . . . . . . . 20 Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k
272		dfaddc2 4381	. . . . . . . . . . . . . . . . . . . . 21 1_c Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k
273	272	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . 20 1_c Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k
274	271, 273	bitr4i 243	. . . . . . . . . . . . . . . . . . 19 Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c 1_c
275	269, 270, 274	3bitri 262	. . . . . . . . . . . . . . . . . 18 Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c 1_c
276	268, 275	anbi12i 678	. . . . . . . . . . . . . . . . 17 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c $/\$ Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ 1_c
277	34, 35, 276	3bitri 262	. . . . . . . . . . . . . . . 16 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ 1_c
278	277	exbii 1582	. . . . . . . . . . . . . . 15 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c $/\$ 1_c
279	22, 30, 278	3bitri 262	. . . . . . . . . . . . . 14 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ 1_c
280	121, 93	addcex 4394	. . . . . . . . . . . . . . 15
281		addceq1 4383	. . . . . . . . . . . . . . . 16 1_c 1_c
282	281	eqeq2d 2364	. . . . . . . . . . . . . . 15 1_c 1_c
283	280, 282	ceqsexv 2894	. . . . . . . . . . . . . 14 $/\$ 1_c 1_c
284	20, 279, 283	3bitri 262	. . . . . . . . . . . . 13 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c 1_c
285	284	rexbii 2639	. . . . . . . . . . . 12 Nn $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn 1_c
286	8, 16, 285	3bitri 262	. . . . . . . . . . 11 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn Nn 1_c
287	121, 122	opkelxpk 4248	. . . . . . . . . . . . . 14 _k $/\$
288	122, 287	mpbiran2 885	. . . . . . . . . . . . 13 _k
289	121	elsnc 3756	. . . . . . . . . . . . 13
290	288, 289	bitri 240	. . . . . . . . . . . 12 _k
291	290	notbii 287	. . . . . . . . . . 11 _k
292	286, 291	anbi12i 678	. . . . . . . . . 10 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn $/\$ _k Nn 1_c $/\$
293		eldif 3221	. . . . . . . . . 10 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn $/\$ _k
294		ancom 437	. . . . . . . . . . 11 $/\$ Nn 1_c Nn 1_c $/\$
295		df-ne 2518	. . . . . . . . . . . 12
296	295	anbi2i 675	. . . . . . . . . . 11 Nn 1_c $/\$ Nn 1_c $/\$
297	294, 296	bitri 240	. . . . . . . . . 10 $/\$ Nn 1_c Nn 1_c $/\$
298	292, 293, 297	3bitr4i 268	. . . . . . . . 9 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ Nn 1_c
299	6, 298	syl6bb 252	. . . . . . . 8 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ Nn 1_c
300	299	pm5.32i 618	. . . . . . 7 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ $/\$ Nn 1_c
301	300	2exbii 1583	. . . . . 6 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ $/\$ Nn 1_c
302	5, 301	bitr3i 242	. . . . 5 $/\$ ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ $/\$ Nn 1_c
303	2, 4, 302	3bitri 262	. . . 4 _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ $/\$ Nn 1_c
304	303	abbi2i 2464	. . 3 _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k $/\$ $/\$ Nn 1_c
305	1, 304	eqtr4i 2376	. 2 _fin _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
306		vvex 4109	. . . 4
307	306, 306	xpkex 4289	. . 3 _k
308		ssetkex 4294	. . . . . . . . . . . . . . 15 S_k
309	308	sikex 4297	. . . . . . . . . . . . . 14 SI_k S_k
310	309	sikex 4297	. . . . . . . . . . . . 13 SI_k SI_k S_k
311	310	sikex 4297	. . . . . . . . . . . 12 SI_k SI_k SI_k S_k
312	311	sikex 4297	. . . . . . . . . . 11 SI_k SI_k SI_k SI_k S_k
313	312	ins3kex 4308	. . . . . . . . . 10 Ins3_k SI_k SI_k SI_k SI_k S_k
314	310	ins3kex 4308	. . . . . . . . . . . . . 14 Ins3_k SI_k SI_k S_k
315	314	ins2kex 4307	. . . . . . . . . . . . 13 Ins2_k Ins3_k SI_k SI_k S_k
316	308	ins3kex 4308	. . . . . . . . . . . . . . . . . 18 Ins3_k S_k
317	316	ins2kex 4307	. . . . . . . . . . . . . . . . 17 Ins2_k Ins3_k S_k
318	317	ins2kex 4307	. . . . . . . . . . . . . . . 16 Ins2_k Ins2_k Ins3_k S_k
319	318	ins2kex 4307	. . . . . . . . . . . . . . 15 Ins2_k Ins2_k Ins2_k Ins3_k S_k
320	308	ins2kex 4307	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k S_k
321	316, 320	inex 4105	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3_k S_k Ins2_k S_k
322		1cex 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1_c
323	322	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ₁ 1_c
324	323	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ ₁ 1_c
325	321, 324	imakex 4300	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
326	325	complex 4104	. . . . . . . . . . . . . . . . . . . . . . . 24 ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
327	326	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . 23 SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
328	327	sikex 4297	. . . . . . . . . . . . . . . . . . . . . 22 SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
329	328	sikex 4297	. . . . . . . . . . . . . . . . . . . . 21 SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
330	329	sikex 4297	. . . . . . . . . . . . . . . . . . . 20 SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
331	330	sikex 4297	. . . . . . . . . . . . . . . . . . 19 SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
332	331	sikex 4297	. . . . . . . . . . . . . . . . . 18 SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
333	332	sikex 4297	. . . . . . . . . . . . . . . . 17 SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
334	333	ins3kex 4308	. . . . . . . . . . . . . . . 16 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c
335	312	sikex 4297	. . . . . . . . . . . . . . . . . . . . . 22 SI_k SI_k SI_k SI_k SI_k S_k
336	335	ins3kex 4308	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
337	336	ins2kex 4307	. . . . . . . . . . . . . . . . . . . 20 Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
338	337	ins2kex 4307	. . . . . . . . . . . . . . . . . . 19 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k
339	335	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . . 24 SI_k SI_k SI_k SI_k SI_k SI_k S_k
340	339	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . 23 SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
341	340	sikex 4297	. . . . . . . . . . . . . . . . . . . . . 22 SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
342	341	sikex 4297	. . . . . . . . . . . . . . . . . . . . 21 SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
343	342	ins3kex 4308	. . . . . . . . . . . . . . . . . . . 20 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
344	340	ins3kex 4308	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
345	344	ins2kex 4307	. . . . . . . . . . . . . . . . . . . 20 Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
346	343, 345	unex 4106	. . . . . . . . . . . . . . . . . . 19 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
347	338, 346	symdifex 4108	. . . . . . . . . . . . . . . . . 18 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k
348	324	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ ₁ ₁ 1_c
349	348	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ ₁ ₁ 1_c
350	349	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . 24 ₁ ₁ ₁ ₁ ₁ 1_c
351	350	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ ₁ ₁ ₁ ₁ 1_c
352	351	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
353	352	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
354	353	pw1ex 4303	. . . . . . . . . . . . . . . . . . . 20 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
355	354	pw1ex 4303	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
356	355	pw1ex 4303	. . . . . . . . . . . . . . . . . 18 ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
357	347, 356	imakex 4300	. . . . . . . . . . . . . . . . 17 Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
358	357	complex 4104	. . . . . . . . . . . . . . . 16 ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
359	334, 358	inex 4105	. . . . . . . . . . . . . . 15 Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
360	319, 359	inex 4105	. . . . . . . . . . . . . 14 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
361	360, 353	imakex 4300	. . . . . . . . . . . . 13 Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
362	315, 361	inex 4105	. . . . . . . . . . . 12 Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c
363	362, 351	imakex 4300	. . . . . . . . . . 11 Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
364	363	ins2kex 4307	. . . . . . . . . 10 Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
365	313, 364	symdifex 4108	. . . . . . . . 9 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
366	365, 351	imakex 4300	. . . . . . . 8 Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
367	366	complex 4104	. . . . . . 7 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c
368		addcexlem 4382	. . . . . . . . . . 11 Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c
369	368, 324	imakex 4300	. . . . . . . . . 10 Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
370	369	imagekex 4312	. . . . . . . . 9 Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
371	370	ins2kex 4307	. . . . . . . 8 Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
372	371	ins2kex 4307	. . . . . . 7 Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
373	367, 372	inex 4105	. . . . . 6 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
374	373, 348	imakex 4300	. . . . 5 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
375		nncex 4396	. . . . . . 7 Nn
376	375	pw1ex 4303	. . . . . 6 ₁ Nn
377	376	pw1ex 4303	. . . . 5 ₁ ₁ Nn
378	374, 377	imakex 4300	. . . 4 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn
379		snex 4111	. . . . 5
380	379, 306	xpkex 4289	. . . 4 _k
381	378, 380	difex 4107	. . 3 ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
382	307, 381	inex 4105	. 2 _k ∼ Ins3_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins2_k Ins3_k SI_k SI_k S_k Ins2_k Ins2_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c ∼ Ins2_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k S_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k Ins2_k Ins3_k SI_k SI_k SI_k SI_k SI_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins2_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ ₁ Nn _k
383	305, 382	eqeltri 2423	1 _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

wne 2516

wrex 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cun 3207

cin 3208

csymdif 3209

c0 3550

csn 3737

copk 4057 1_cc1c 4134

₁ cpw1 4135

_k cxpk 4174 Ins2_k cins2k 4176 Ins3_k cins3k 4177

_kcimak 4179 SI_k csik 4181 Image_kcimagek 4182 S_k cssetk 4183 Nn cnnc 4373

cplc 4375

_fin cltfin 4433

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 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-sbc 3047 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-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-addc 4378 df-nnc 4379 df-ltfin 4441

This theorem is referenced by: ltfintrilem1 4465

W3C validator