ncfinraiselem2 - New Foundations Explorer

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

Theorem ncfinraiselem2 4480

Description: Lemma for ncfinraise 4481. Show stratification for induction. (Contributed by SF, 22-Jan-2015.)

**Assertion**
Ref	Expression
ncfinraiselem2	Nn ₁ $/\$ ₁

Distinct variable groups:

Proof of Theorem ncfinraiselem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4111	. . . . . 6
2	1	elcompl 3225	. . . . 5 ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
3	1	elimak 4259	. . . . . 6 SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
4		elpw11c 4147	. . . . . . . . . 10 ₁ 1_c
5	4	anbi1i 676	. . . . . . . . 9 ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
6		19.41v 1901	. . . . . . . . 9 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
7	5, 6	bitr4i 243	. . . . . . . 8 ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
8	7	exbii 1582	. . . . . . 7 ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
9		df-rex 2620	. . . . . . 7 ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
10		excom 1741	. . . . . . 7 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
11	8, 9, 10	3bitr4i 268	. . . . . 6 ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
12		snex 4111	. . . . . . . . . 10
13		opkeq1 4059	. . . . . . . . . . 11
14	13	eleq1d 2419	. . . . . . . . . 10 SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
15	12, 14	ceqsexv 2894	. . . . . . . . 9 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
16		elin 3219	. . . . . . . . 9 SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c SI_k S_k $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c
17		snex 4111	. . . . . . . . . . . 12
18		vex 2862	. . . . . . . . . . . 12
19	17, 18	opksnelsik 4265	. . . . . . . . . . 11 SI_k S_k S_k
20		vex 2862	. . . . . . . . . . . 12
21	20, 18	elssetk 4270	. . . . . . . . . . 11 S_k
22	19, 21	bitri 240	. . . . . . . . . 10 SI_k S_k
23		opkex 4113	. . . . . . . . . . . . 13
24	23	elimak 4259	. . . . . . . . . . . 12 Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
25		df-rex 2620	. . . . . . . . . . . 12 ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
26		elpw131c 4149	. . . . . . . . . . . . . . . 16 ₁ ₁ ₁ 1_c
27	26	anbi1i 676	. . . . . . . . . . . . . . 15 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
28		19.41v 1901	. . . . . . . . . . . . . . 15 $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
29	27, 28	bitr4i 243	. . . . . . . . . . . . . 14 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
30	29	exbii 1582	. . . . . . . . . . . . 13 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
31		excom 1741	. . . . . . . . . . . . 13 $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
32	30, 31	bitr4i 243	. . . . . . . . . . . 12 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
33	24, 25, 32	3bitri 262	. . . . . . . . . . 11 Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
34		snex 4111	. . . . . . . . . . . . . . 15
35		opkeq1 4059	. . . . . . . . . . . . . . . 16
36	35	eleq1d 2419	. . . . . . . . . . . . . . 15 Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
37	34, 36	ceqsexv 2894	. . . . . . . . . . . . . 14 $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
38		eldif 3221	. . . . . . . . . . . . . 14 Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c Ins2_k SI_k S_k $/\$ Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
39		snex 4111	. . . . . . . . . . . . . . . . 17
40	39, 12, 1	otkelins2k 4255	. . . . . . . . . . . . . . . 16 Ins2_k SI_k S_k SI_k S_k
41		snex 4111	. . . . . . . . . . . . . . . . 17
42	41, 18	opksnelsik 4265	. . . . . . . . . . . . . . . 16 SI_k S_k S_k
43		vex 2862	. . . . . . . . . . . . . . . . 17
44	43, 18	elssetk 4270	. . . . . . . . . . . . . . . 16 S_k
45	40, 42, 44	3bitri 262	. . . . . . . . . . . . . . 15 Ins2_k SI_k S_k
46	39, 12, 1	otkelins3k 4256	. . . . . . . . . . . . . . . . 17 Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c
47		df-rex 2620	. . . . . . . . . . . . . . . . . . 19 ₁ 1_c ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
48		elpw11c 4147	. . . . . . . . . . . . . . . . . . . . . 22 ₁ 1_c
49	48	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
50		19.41v 1901	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
51	49, 50	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
52	51	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
53	47, 52	bitri 240	. . . . . . . . . . . . . . . . . 18 ₁ 1_c ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
54		opkex 4113	. . . . . . . . . . . . . . . . . . 19
55	54	elimak 4259	. . . . . . . . . . . . . . . . . 18 ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c ₁ 1_c ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
56		excom 1741	. . . . . . . . . . . . . . . . . 18 $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
57	53, 55, 56	3bitr4i 268	. . . . . . . . . . . . . . . . 17 ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
58		snex 4111	. . . . . . . . . . . . . . . . . . . . 21
59		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . 22
60	59	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
61	58, 60	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . 20 $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
62		elin 3219	. . . . . . . . . . . . . . . . . . . 20 ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ Nn _k $/\$ Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
63	58, 54	opkelxpk 4248	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ Nn _k ₁ ₁ Nn $/\$
64	54, 63	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ Nn _k ₁ ₁ Nn
65		snelpw1 4146	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ Nn ₁ Nn
66		snelpw1 4146	. . . . . . . . . . . . . . . . . . . . . 22 ₁ Nn Nn
67	64, 65, 66	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ Nn _k Nn
68		elin 3219	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
69		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	69, 39, 12	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
71		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
73		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
74		elpw121c 4148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ₁ ₁ 1_c
75	74	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
76		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
77	75, 76	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
78	77	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
79		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
80	78, 79	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
81	72, 73, 80	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
82		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
84	83	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
85	82, 84	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
86		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins3_k S_k
87		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
88	87, 69, 12	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c
89		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90	89, 17	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c
91	89, 20	eqpw1relk 4479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
92	88, 90, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
93	87, 69, 12	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3_k S_k S_k
94	89, 69	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 S_k
95	93, 94	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3_k S_k
96	92, 95	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins3_k S_k ₁ $/\$
97	85, 86, 96	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁ $/\$
98	97	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁ $/\$
99		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ $/\$
100	98, 99	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁
101	70, 81, 100	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁
102		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . 26
103	102	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
104	74	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
105		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
106	104, 105	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
107	106	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
108		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁ ₁ 1_c $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
109		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
110	107, 108, 109	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
111		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
112	111	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
113	82, 112	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k
114		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins3_k S_k
115	87, 69, 39	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c
116	89, 41	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c
117	89, 43	eqpw1relk 4479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
118	115, 116, 117	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
119	87, 69, 39	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3_k S_k S_k
120	119, 94	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3_k S_k
121	118, 120	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins3_k S_k ₁ $/\$
122	113, 114, 121	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁ $/\$
123	122	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k ₁ $/\$
124	103, 110, 123	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ $/\$
125	69, 39, 12	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
126		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . 24 ₁ ₁ $/\$
127	124, 125, 126	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁
128	101, 127	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ $/\$ ₁
129	68, 128	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ $/\$ ₁
130	67, 129	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 ₁ ₁ Nn _k $/\$ Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ ₁ $/\$ ₁
131	61, 62, 130	3bitri 262	. . . . . . . . . . . . . . . . . . 19 $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ ₁ $/\$ ₁
132	131	exbii 1582	. . . . . . . . . . . . . . . . . 18 $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ ₁ $/\$ ₁
133		df-rex 2620	. . . . . . . . . . . . . . . . . 18 Nn ₁ $/\$ ₁ Nn $/\$ ₁ $/\$ ₁
134	132, 133	bitr4i 243	. . . . . . . . . . . . . . . . 17 $/\$ ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn ₁ $/\$ ₁
135	46, 57, 134	3bitri 262	. . . . . . . . . . . . . . . 16 Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c Nn ₁ $/\$ ₁
136	135	notbii 287	. . . . . . . . . . . . . . 15 Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c Nn ₁ $/\$ ₁
137	45, 136	anbi12i 678	. . . . . . . . . . . . . 14 Ins2_k SI_k S_k $/\$ Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Nn ₁ $/\$ ₁
138	37, 38, 137	3bitri 262	. . . . . . . . . . . . 13 $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Nn ₁ $/\$ ₁
139	138	exbii 1582	. . . . . . . . . . . 12 $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c $/\$ Nn ₁ $/\$ ₁
140		df-rex 2620	. . . . . . . . . . . 12 Nn ₁ $/\$ ₁ $/\$ Nn ₁ $/\$ ₁
141	139, 140	bitr4i 243	. . . . . . . . . . 11 $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c Nn ₁ $/\$ ₁
142		rexnal 2625	. . . . . . . . . . 11 Nn ₁ $/\$ ₁ Nn ₁ $/\$ ₁
143	33, 141, 142	3bitri 262	. . . . . . . . . 10 Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c Nn ₁ $/\$ ₁
144	22, 143	anbi12i 678	. . . . . . . . 9 SI_k S_k $/\$ Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Nn ₁ $/\$ ₁
145	15, 16, 144	3bitri 262	. . . . . . . 8 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k ₁ ₁ Nn _k Ins2_k Ins2_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁