sfintfinlem1 - New Foundations Explorer

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

Theorem sfintfinlem1 4531

Description: Lemma for sfintfin 4532. 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 2862	. . . . 5
2	1	eluni1 4173	. . . 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 4111	. . . . . . . 8
4	3	elimak 4259	. . . . . . 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 4139	. . . . . . . . . . 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 2620	. . . . . . . 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 4111	. . . . . . . . . 10
14		opkeq1 4059	. . . . . . . . . . 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 2894	. . . . . . . . 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 4250	. . . . . . . . 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 3221	. . . . . . . . . 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 2862	. . . . . . . . . . . . 13
20	1, 19	opksnelsik 4265	. . . . . . . . . . . 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 4524	. . . . . . . . . . . 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 4113	. . . . . . . . . . . . . . 15
24	23	elimak 4259	. . . . . . . . . . . . . 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 2620	. . . . . . . . . . . . . 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 4147	. . . . . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . . 16
35		opkeq1 4059	. . . . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . . . 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 3219	. . . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . . . . 18
40	39, 3, 13	otkelins2k 4255	. . . . . . . . . . . . . . . . 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 4250	. . . . . . . . . . . . . . . . 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 4486	. . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . 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 4113	. . . . . . . . . . . . . . . . . . 19
46	45	elimak 4259	. . . . . . . . . . . . . . . . . 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 4147	. . . . . . . . . . . . . . . . . . . . . 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 2620	. . . . . . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . . . . . . . 21
56		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . . . . . . . . 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 3219	. . . . . . . . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . . . . . . . . . 23
61	60, 39, 3	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . 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 4250	. . . . . . . . . . . . . . . . . . . . . 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 4486	. . . . . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . . . . 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 4524	. . . . . . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . . 18 T_fin
73		sfineq1 4526	. . . . . . . . . . . . . . . . . 18 T_fin S_fin S_fin T_fin
74	72, 73	ceqsexv 2894	. . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . 14 T_fin
80		sfineq2 4527	. . . . . . . . . . . . . 14 T_fin S_fin T_fin S_fin T_fin T_fin
81	79, 80	ceqsexv 2894	. . . . . . . . . . . . 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 3225	. . . . 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	abbi2i 2464	. 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 4525	. . . . . . . 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 4297	. . . . . . 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 4487	. . . . . . . . . . 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 4287	. . . . . . . . . 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 4307	. . . . . . . . 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 4308	. . . . . . . . . . . 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 4105	. . . . . . . . . . 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 4142	. . . . . . . . . . . 12 1_c
104	103	pw1ex 4303	. . . . . . . . . . 11 ₁ 1_c
105	102, 104	imakex 4300	. . . . . . . . . 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 4308	. . . . . . . . 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 4105	. . . . . . . 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 4300	. . . . . . 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 4107	. . . . . 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 4287	. . . . 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 4300	. . . 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 4104	. . 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 4293	. 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 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cun 3207

cin 3208

csymdif 3209

c0 3550

cpw 3722

csn 3737

copk 4057 ⋃₁cuni1 4133 1_cc1c 4134

₁ cpw1 4135

_k cxpk 4174

_kccnvk 4175 Ins2_k cins2k 4176 Ins3_k cins3k 4177

_kcimak 4179 SI_k csik 4181 S_k cssetk 4183

_k cidk 4184 Nn cnnc 4373 T_fin ctfin 4435 S_fin wsfin 4438

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

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

This theorem is referenced by: sfintfin 4532

W3C validator