sfintfinlem1 - New Foundations Explorer

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

Theorem sfintfinlem1 4532

Description: Lemma for sfintfin 4533. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)

**Assertion**
Ref	Expression
sfintfinlem1	S_fin S_fin T_fin T_fin

Distinct variable group:

Proof of Theorem sfintfinlem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . 5
2	1	eluni1 4174	. . . 4 ⋃₁ ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c
3		snex 4112	. . . . . . . 8
4	3	elimak 4260	. . . . . . 7 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
5		el1c 4140	. . . . . . . . . . 11 1_c
6	5	anbi1i 676	. . . . . . . . . 10 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
7		19.41v 1901	. . . . . . . . . 10 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
8	6, 7	bitr4i 243	. . . . . . . . 9 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
9	8	exbii 1582	. . . . . . . 8 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
10		df-rex 2621	. . . . . . . 8 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
11		excom 1741	. . . . . . . 8 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
12	9, 10, 11	3bitr4i 268	. . . . . . 7 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
13		snex 4112	. . . . . . . . . 10
14		opkeq1 4060	. . . . . . . . . . 11
15	14	eleq1d 2419	. . . . . . . . . 10 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
16	13, 15	ceqsexv 2895	. . . . . . . . 9 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
17	13, 3	opkelcnvk 4251	. . . . . . . . 9 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
18		eldif 3222	. . . . . . . . . 10 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
19		vex 2863	. . . . . . . . . . . . 13
20	1, 19	opksnelsik 4266	. . . . . . . . . . . 12 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
21	1, 19	srelk 4525	. . . . . . . . . . . 12 Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin
22	20, 21	bitri 240	. . . . . . . . . . 11 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin
23		opkex 4114	. . . . . . . . . . . . . . 15
24	23	elimak 4260	. . . . . . . . . . . . . 14 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
25		df-rex 2621	. . . . . . . . . . . . . 14 ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
26		elpw11c 4148	. . . . . . . . . . . . . . . . . 18 ₁ 1_c
27	26	anbi1i 676	. . . . . . . . . . . . . . . . 17 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
28		19.41v 1901	. . . . . . . . . . . . . . . . 17 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
29	27, 28	bitr4i 243	. . . . . . . . . . . . . . . 16 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
30	29	exbii 1582	. . . . . . . . . . . . . . 15 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
31		excom 1741	. . . . . . . . . . . . . . 15 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
32	30, 31	bitr4i 243	. . . . . . . . . . . . . 14 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
33	24, 25, 32	3bitri 262	. . . . . . . . . . . . 13 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
34		snex 4112	. . . . . . . . . . . . . . . 16
35		opkeq1 4060	. . . . . . . . . . . . . . . . 17
36	35	eleq1d 2419	. . . . . . . . . . . . . . . 16 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
37	34, 36	ceqsexv 2895	. . . . . . . . . . . . . . 15 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
38		elin 3220	. . . . . . . . . . . . . . 15 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $/\$ Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
39		vex 2863	. . . . . . . . . . . . . . . . . 18
40	39, 3, 13	otkelins2k 4256	. . . . . . . . . . . . . . . . 17 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
41	39, 13	opkelcnvk 4251	. . . . . . . . . . . . . . . . 17 _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
42	19, 39	eqtfinrelk 4487	. . . . . . . . . . . . . . . . 17 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin
43	40, 41, 42	3bitri 262	. . . . . . . . . . . . . . . 16 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin
44	39, 3, 13	otkelins3k 4257	. . . . . . . . . . . . . . . . 17 Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
45		opkex 4114	. . . . . . . . . . . . . . . . . . 19
46	45	elimak 4260	. . . . . . . . . . . . . . . . . 18 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
47		elpw11c 4148	. . . . . . . . . . . . . . . . . . . . . 22 ₁ 1_c
48	47	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
49		19.41v 1901	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
50	48, 49	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
51	50	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
52		df-rex 2621	. . . . . . . . . . . . . . . . . . 19 ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
53		excom 1741	. . . . . . . . . . . . . . . . . . 19 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
54	51, 52, 53	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
55		snex 4112	. . . . . . . . . . . . . . . . . . . . 21
56		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22
57	56	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
58	55, 57	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . 20 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
59		elin 3220	. . . . . . . . . . . . . . . . . . . 20 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $/\$ Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
60		vex 2863	. . . . . . . . . . . . . . . . . . . . . . 23
61	60, 39, 3	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
62	60, 3	opkelcnvk 4251	. . . . . . . . . . . . . . . . . . . . . 22 _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
63	1, 60	eqtfinrelk 4487	. . . . . . . . . . . . . . . . . . . . . 22 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin
64	61, 62, 63	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin
65	60, 39, 3	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . 22 Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
66	60, 39	srelk 4525	. . . . . . . . . . . . . . . . . . . . . 22 Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin
67	65, 66	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin
68	64, 67	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $/\$ Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c T_fin $/\$ S_fin
69	58, 59, 68	3bitri 262	. . . . . . . . . . . . . . . . . . 19 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c T_fin $/\$ S_fin
70	69	exbii 1582	. . . . . . . . . . . . . . . . . 18 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c T_fin $/\$ S_fin
71	46, 54, 70	3bitri 262	. . . . . . . . . . . . . . . . 17 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c T_fin $/\$ S_fin
72		tfinex 4486	. . . . . . . . . . . . . . . . . 18 T_fin
73		sfineq1 4527	. . . . . . . . . . . . . . . . . 18 T_fin S_fin S_fin T_fin
74	72, 73	ceqsexv 2895	. . . . . . . . . . . . . . . . 17 T_fin $/\$ S_fin S_fin T_fin
75	44, 71, 74	3bitri 262	. . . . . . . . . . . . . . . 16 Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c S_fin T_fin
76	43, 75	anbi12i 678	. . . . . . . . . . . . . . 15 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k $/\$ Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c T_fin $/\$ S_fin T_fin
77	37, 38, 76	3bitri 262	. . . . . . . . . . . . . 14 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c T_fin $/\$ S_fin T_fin
78	77	exbii 1582	. . . . . . . . . . . . 13 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c T_fin $/\$ S_fin T_fin
79		tfinex 4486	. . . . . . . . . . . . . 14 T_fin
80		sfineq2 4528	. . . . . . . . . . . . . 14 T_fin S_fin T_fin S_fin T_fin T_fin
81	79, 80	ceqsexv 2895	. . . . . . . . . . . . 13 T_fin $/\$ S_fin T_fin S_fin T_fin T_fin
82	33, 78, 81	3bitri 262	. . . . . . . . . . . 12 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c S_fin T_fin T_fin
83	82	notbii 287	. . . . . . . . . . 11 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c S_fin T_fin T_fin
84	22, 83	anbi12i 678	. . . . . . . . . 10 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c S_fin $/\$ S_fin T_fin T_fin
85		annim 414	. . . . . . . . . 10 S_fin $/\$ S_fin T_fin T_fin S_fin S_fin T_fin T_fin
86	18, 84, 85	3bitri 262	. . . . . . . . 9 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c S_fin S_fin T_fin T_fin
87	16, 17, 86	3bitri 262	. . . . . . . 8 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c S_fin S_fin T_fin T_fin
88	87	exbii 1582	. . . . . . 7 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c S_fin S_fin T_fin T_fin
89	4, 12, 88	3bitri 262	. . . . . 6 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c S_fin S_fin T_fin T_fin
90	89	notbii 287	. . . . 5 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c S_fin S_fin T_fin T_fin
91	3	elcompl 3226	. . . . 5 ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c
92		alex 1572	. . . . 5 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
93	90, 91, 92	3bitr4i 268	. . . 4 ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c S_fin S_fin T_fin T_fin
94	2, 93	bitri 240	. . 3 ⋃₁ ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c S_fin S_fin T_fin T_fin
95	94	eqabi 2465	. 2 ⋃₁ ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c S_fin S_fin T_fin T_fin
96		srelkex 4526	. . . . . . . 8 Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
97	96	sikex 4298	. . . . . . 7 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
98		tfinrelkex 4488	. . . . . . . . . . 11 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
99	98	cnvkex 4288	. . . . . . . . . 10 _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
100	99	ins2kex 4308	. . . . . . . . 9 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
101	96	ins3kex 4309	. . . . . . . . . . . 12 Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
102	100, 101	inex 4106	. . . . . . . . . . 11 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
103		1cex 4143	. . . . . . . . . . . 12 1_c
104	103	pw1ex 4304	. . . . . . . . . . 11 ₁ 1_c
105	102, 104	imakex 4301	. . . . . . . . . 10 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
106	105	ins3kex 4309	. . . . . . . . 9 Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
107	100, 106	inex 4106	. . . . . . . 8 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
108	107, 104	imakex 4301	. . . . . . 7 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
109	97, 108	difex 4108	. . . . . 6 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
110	109	cnvkex 4288	. . . . 5 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
111	110, 103	imakex 4301	. . . 4 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c
112	111	complex 4105	. . 3 ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c
113	112	uni1ex 4294	. 2 ⋃₁ ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c
114	95, 113	eqeltrri 2424	1 S_fin S_fin T_fin T_fin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 358

wal 1540

wex 1541

wceq 1642

wcel 1710

cab 2339

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cun 3208

cin 3209

csymdif 3210

c0 3551

cpw 3723

csn 3738

copk 4058 ⋃₁cuni1 4134 1_cc1c 4135

₁ cpw1 4136

_k cxpk 4175

_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178

_kcimak 4180 SI_k csik 4182 S_k cssetk 4184

_k cidk 4185 Nn cnnc 4374 T_fin ctfin 4436 S_fin wsfin 4439

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

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-eu 2208 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-addc 4379 df-nnc 4380 df-tfin 4444 df-sfin 4447

This theorem is referenced by: sfintfin 4533

W3C validator