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