nnpweqlem1 - New Foundations Explorer

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

Theorem nnpweqlem1 4523

Description: Lemma for nnpweq 4524. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)

**Assertion**
Ref	Expression
nnpweqlem1	Nn $/\$

Distinct variable group:

Proof of Theorem nnpweqlem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . 5
2	1	eluni1 4174	. . . 4 ⋃₁ ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c
3		snex 4112	. . . . . . . . . 10
4		opkeq1 4060	. . . . . . . . . . 11
5	4	eleq1d 2419	. . . . . . . . . 10 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
6	3, 5	ceqsexv 2895	. . . . . . . . 9 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
7		elin 3220	. . . . . . . . 9 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c SI_k S_k $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
8		snex 4112	. . . . . . . . . . . 12
9	8, 1	opksnelsik 4266	. . . . . . . . . . 11 SI_k S_k S_k
10		vex 2863	. . . . . . . . . . . 12
11	10, 1	elssetk 4271	. . . . . . . . . . 11 S_k
12	9, 11	bitri 240	. . . . . . . . . 10 SI_k S_k
13		opkex 4114	. . . . . . . . . . . . 13
14	13	elimak 4260	. . . . . . . . . . . 12 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
15		elpw131c 4150	. . . . . . . . . . . . . . . 16 ₁ ₁ ₁ 1_c
16	15	anbi1i 676	. . . . . . . . . . . . . . 15 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
17		19.41v 1901	. . . . . . . . . . . . . . 15 $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
18	16, 17	bitr4i 243	. . . . . . . . . . . . . 14 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
19	18	exbii 1582	. . . . . . . . . . . . 13 ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
20		df-rex 2621	. . . . . . . . . . . . 13 ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn ₁ ₁ ₁ 1_c $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
21		excom 1741	. . . . . . . . . . . . 13 $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
22	19, 20, 21	3bitr4i 268	. . . . . . . . . . . 12 ₁ ₁ ₁ 1_c Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
23		snex 4112	. . . . . . . . . . . . . . 15
24		opkeq1 4060	. . . . . . . . . . . . . . . 16
25	24	eleq1d 2419	. . . . . . . . . . . . . . 15 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
26	23, 25	ceqsexv 2895	. . . . . . . . . . . . . 14 $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
27		eldif 3222	. . . . . . . . . . . . . 14 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Ins2_k SI_k S_k $/\$ Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
28		snex 4112	. . . . . . . . . . . . . . . . 17
29		snex 4112	. . . . . . . . . . . . . . . . 17
30	28, 3, 29	otkelins2k 4256	. . . . . . . . . . . . . . . 16 Ins2_k SI_k S_k SI_k S_k
31		snex 4112	. . . . . . . . . . . . . . . . 17
32	31, 1	opksnelsik 4266	. . . . . . . . . . . . . . . 16 SI_k S_k S_k
33		vex 2863	. . . . . . . . . . . . . . . . 17
34	33, 1	elssetk 4271	. . . . . . . . . . . . . . . 16 S_k
35	30, 32, 34	3bitri 262	. . . . . . . . . . . . . . 15 Ins2_k SI_k S_k
36	28, 3, 29	otkelins3k 4257	. . . . . . . . . . . . . . . . 17 Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
37		opkex 4114	. . . . . . . . . . . . . . . . . . 19
38	37	elimak 4260	. . . . . . . . . . . . . . . . . 18 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn ₁ ₁ Nn Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
39		elpw12 4146	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ Nn Nn
40	39	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
41		r19.41v 2765	. . . . . . . . . . . . . . . . . . . . 21 Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
42	40, 41	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 ₁ ₁ Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
43	42	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
44		df-rex 2621	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ Nn Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
45		rexcom4 2879	. . . . . . . . . . . . . . . . . . 19 Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
46	43, 44, 45	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ₁ ₁ Nn Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
47	38, 46	bitri 240	. . . . . . . . . . . . . . . . 17 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
48		snex 4112	. . . . . . . . . . . . . . . . . . . 20
49		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . 21
50	49	eleq1d 2419	. . . . . . . . . . . . . . . . . . . 20 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
51	48, 50	ceqsexv 2895	. . . . . . . . . . . . . . . . . . 19 $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
52		elin 3220	. . . . . . . . . . . . . . . . . . 19 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
53		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . 23
54	53	elimak 4260	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
55		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ₁ ₁ 1_c
56	55	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ 1_c $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
57		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
58	56, 57	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ₁ ₁ 1_c $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
59	58	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ 1_c $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
60		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ 1_c Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k ₁ ₁ 1_c $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
61		excom 1741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
62	59, 60, 61	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ 1_c Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
63		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25
64		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . 26
65	64	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
66	63, 65	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
67		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c $/\$ Ins3_k S_k
68		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
70	68, 69, 3	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
71		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
72	71, 8	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . 26 SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
73	71, 8	opkelcnvk 4251	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
74	10, 71	eqpwrelk 4479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
75	73, 74	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
76	70, 72, 75	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
77	68, 69, 3	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3_k S_k S_k
78	71, 69	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 S_k
79	77, 78	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3_k S_k
80	76, 79	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c $/\$ Ins3_k S_k $/\$
81	66, 67, 80	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$
82	81	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$
83	54, 62, 82	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$
84	69, 28, 3	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
85		df-clel 2349	. . . . . . . . . . . . . . . . . . . . 21 $/\$
86	83, 84, 85	3bitr4i 268	. . . . . . . . . . . . . . . . . . . 20 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
87		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . 23
88	87	elimak 4260	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
89	55	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ 1_c $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
90		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
91	89, 90	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ₁ ₁ 1_c $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
92	91	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ 1_c $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
93		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ 1_c Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k ₁ ₁ 1_c $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
94		excom 1741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
95	92, 93, 94	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ 1_c Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
96		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . 26
97	96	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
98	63, 97	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
99		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c $/\$ Ins3_k S_k
100	68, 69, 28	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
101	68, 28	opkelcnvk 4251	. . . . . . . . . . . . . . . . . . . . . . . . . 26 _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
102	31, 71	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
103	33, 71	eqpwrelk 4479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
104	102, 103	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
105	100, 101, 104	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
106	68, 69, 28	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3_k S_k S_k
107	106, 78	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3_k S_k
108	105, 107	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c $/\$ Ins3_k S_k $/\$
109	98, 99, 108	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$
110	109	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k $/\$
111	88, 95, 110	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$
112	69, 28, 3	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
113		df-clel 2349	. . . . . . . . . . . . . . . . . . . . 21 $/\$
114	111, 112, 113	3bitr4i 268	. . . . . . . . . . . . . . . . . . . 20 Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
115	86, 114	anbi12i 678	. . . . . . . . . . . . . . . . . . 19 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$
116	51, 52, 115	3bitri 262	. . . . . . . . . . . . . . . . . 18 $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c $/\$
117	116	rexbii 2640	. . . . . . . . . . . . . . . . 17 Nn $/\$ Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Nn $/\$
118	36, 47, 117	3bitri 262	. . . . . . . . . . . . . . . 16 Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Nn $/\$
119	118	notbii 287	. . . . . . . . . . . . . . 15 Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn Nn $/\$
120	35, 119	anbi12i 678	. . . . . . . . . . . . . 14 Ins2_k SI_k S_k $/\$ Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Nn $/\$
121	26, 27, 120	3bitri 262	. . . . . . . . . . . . 13 $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Nn $/\$
122	121	exbii 1582	. . . . . . . . . . . 12 $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn $/\$ Nn $/\$
123	14, 22, 122	3bitri 262	. . . . . . . . . . 11 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ Nn $/\$
124		df-rex 2621	. . . . . . . . . . 11 Nn $/\$ $/\$ Nn $/\$
125		rexnal 2626	. . . . . . . . . . 11 Nn $/\$ Nn $/\$
126	123, 124, 125	3bitr2i 264	. . . . . . . . . 10 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c Nn $/\$
127	12, 126	anbi12i 678	. . . . . . . . 9 SI_k S_k $/\$ Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ Nn $/\$
128	6, 7, 127	3bitri 262	. . . . . . . 8 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ Nn $/\$
129	128	exbii 1582	. . . . . . 7 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ Nn $/\$
130	29	elimak 4260	. . . . . . . 8 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
131		elpw11c 4148	. . . . . . . . . . . 12 ₁ 1_c
132	131	anbi1i 676	. . . . . . . . . . 11 ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
133		19.41v 1901	. . . . . . . . . . 11 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
134	132, 133	bitr4i 243	. . . . . . . . . 10 ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
135	134	exbii 1582	. . . . . . . . 9 ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
136		df-rex 2621	. . . . . . . . 9 ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
137		excom 1741	. . . . . . . . 9 $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
138	135, 136, 137	3bitr4i 268	. . . . . . . 8 ₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
139	130, 138	bitri 240	. . . . . . 7 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
140		df-rex 2621	. . . . . . 7 Nn $/\$ $/\$ Nn $/\$
141	129, 139, 140	3bitr4i 268	. . . . . 6 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c Nn $/\$
142	141	notbii 287	. . . . 5 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c Nn $/\$
143	29	elcompl 3226	. . . . 5 ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c
144		dfral2 2627	. . . . 5 Nn $/\$ Nn $/\$
145	142, 143, 144	3bitr4i 268	. . . 4 ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c Nn $/\$
146	2, 145	bitri 240	. . 3 ⋃₁ ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c Nn $/\$
147	146	eqabi 2465	. 2 ⋃₁ ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c Nn $/\$
148		ssetkex 4295	. . . . . . 7 S_k
149	148	sikex 4298	. . . . . 6 SI_k S_k
150	149	ins2kex 4308	. . . . . . . 8 Ins2_k SI_k S_k
151	148	ins2kex 4308	. . . . . . . . . . . . . . . . . . . 20 Ins2_k S_k
152	149	ins3kex 4309	. . . . . . . . . . . . . . . . . . . 20 Ins3_k SI_k S_k
153	151, 152	symdifex 4109	. . . . . . . . . . . . . . . . . . 19 Ins2_k S_k Ins3_k SI_k S_k
154		1cex 4143	. . . . . . . . . . . . . . . . . . . . 21 1_c
155	154	pw1ex 4304	. . . . . . . . . . . . . . . . . . . 20 ₁ 1_c
156	155	pw1ex 4304	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ 1_c
157	153, 156	imakex 4301	. . . . . . . . . . . . . . . . . 18 Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
158	157	complex 4105	. . . . . . . . . . . . . . . . 17 ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
159	158	cnvkex 4288	. . . . . . . . . . . . . . . 16 _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
160	159	sikex 4298	. . . . . . . . . . . . . . 15 SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
161	160	ins2kex 4308	. . . . . . . . . . . . . 14 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
162	148	ins3kex 4309	. . . . . . . . . . . . . 14 Ins3_k S_k
163	161, 162	inex 4106	. . . . . . . . . . . . 13 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
164	163, 156	imakex 4301	. . . . . . . . . . . 12 Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
165	164	ins2kex 4308	. . . . . . . . . . 11 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
166	158	sikex 4298	. . . . . . . . . . . . . . . 16 SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
167	166	cnvkex 4288	. . . . . . . . . . . . . . 15 _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
168	167	ins2kex 4308	. . . . . . . . . . . . . 14 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c
169	168, 162	inex 4106	. . . . . . . . . . . . 13 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k
170	169, 156	imakex 4301	. . . . . . . . . . . 12 Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
171	170	ins3kex 4309	. . . . . . . . . . 11 Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
172	165, 171	inex 4106	. . . . . . . . . 10 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c
173		nncex 4397	. . . . . . . . . . . 12 Nn
174	173	pw1ex 4304	. . . . . . . . . . 11 ₁ Nn
175	174	pw1ex 4304	. . . . . . . . . 10 ₁ ₁ Nn
176	172, 175	imakex 4301	. . . . . . . . 9 Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
177	176	ins3kex 4309	. . . . . . . 8 Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
178	150, 177	difex 4108	. . . . . . 7 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn
179	156	pw1ex 4304	. . . . . . 7 ₁ ₁ ₁ 1_c
180	178, 179	imakex 4301	. . . . . 6 Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
181	149, 180	inex 4106	. . . . 5 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c
182	181, 155	imakex 4301	. . . 4 SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c
183	182	complex 4105	. . 3 ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c
184	183	uni1ex 4294	. 2 ⋃₁ ∼ SI_k S_k Ins2_k SI_k S_k Ins3_k Ins2_k Ins2_k SI_k _k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c Ins3_k Ins2_k _k SI_k ∼ Ins2_k S_k Ins3_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k _k₁ ₁ 1_c_k₁ ₁ Nn _k₁ ₁ ₁ 1_c_k₁ 1_c
185	147, 184	eqeltrri 2424	1 Nn $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 358

wex 1541

wceq 1642

wcel 1710

cab 2339

wral 2615

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cin 3209

csymdif 3210

cpw 3723

csn 3738

copk 4058 ⋃₁cuni1 4134 1_cc1c 4135

₁ cpw1 4136

_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178

_kcimak 4180 SI_k csik 4182 S_k cssetk 4184 Nn cnnc 4374

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

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-addc 4379 df-nnc 4380

This theorem is referenced by: nnpweq 4524

W3C validator