nnadjoinlem1 - New Foundations Explorer

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

Theorem nnadjoinlem1 4520

Description: Lemma for nnadjoin 4521. Establish stratification. (Contributed by SF, 29-Jan-2015.)

**Assertion**
Ref	Expression
nnadjoinlem1	∼

Distinct variable group:

Proof of Theorem nnadjoinlem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4112	. . . . . . . . 9
2		opkeq1 4060	. . . . . . . . . 10
3	2	eleq1d 2419	. . . . . . . . 9 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
4	1, 3	ceqsexv 2895	. . . . . . . 8 $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
5		elin 3220	. . . . . . . 8 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c S_k $/\$ ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
6		vex 2863	. . . . . . . . . 10
7		vex 2863	. . . . . . . . . 10
8	6, 7	elssetk 4271	. . . . . . . . 9 S_k
9		eldif 3222	. . . . . . . . . 10 ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ∼ ₁ ₁ _k S_k _k1_c _k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
10	1	elcompl 3226	. . . . . . . . . . . . 13 ∼ ₁ ₁ _k S_k _k1_c ₁ ₁ _k S_k _k1_c
11	6	elimak 4260	. . . . . . . . . . . . . . 15 ₁ _k S_k _k1_c 1_c ₁ _k S_k
12		el1c 4140	. . . . . . . . . . . . . . . . . . 19 1_c
13	12	anbi1i 676	. . . . . . . . . . . . . . . . . 18 1_c $/\$ ₁ _k S_k $/\$ ₁ _k S_k
14		19.41v 1901	. . . . . . . . . . . . . . . . . 18 $/\$ ₁ _k S_k $/\$ ₁ _k S_k
15	13, 14	bitr4i 243	. . . . . . . . . . . . . . . . 17 1_c $/\$ ₁ _k S_k $/\$ ₁ _k S_k
16	15	exbii 1582	. . . . . . . . . . . . . . . 16 1_c $/\$ ₁ _k S_k $/\$ ₁ _k S_k
17		df-rex 2621	. . . . . . . . . . . . . . . 16 1_c ₁ _k S_k 1_c $/\$ ₁ _k S_k
18		excom 1741	. . . . . . . . . . . . . . . 16 $/\$ ₁ _k S_k $/\$ ₁ _k S_k
19	16, 17, 18	3bitr4i 268	. . . . . . . . . . . . . . 15 1_c ₁ _k S_k $/\$ ₁ _k S_k
20		snex 4112	. . . . . . . . . . . . . . . . . 18
21		opkeq1 4060	. . . . . . . . . . . . . . . . . . 19
22	21	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 ₁ _k S_k ₁ _k S_k
23	20, 22	ceqsexv 2895	. . . . . . . . . . . . . . . . 17 $/\$ ₁ _k S_k ₁ _k S_k
24		elin 3220	. . . . . . . . . . . . . . . . 17 ₁ _k S_k ₁ _k $/\$ S_k
25	20, 6	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . 20 ₁ _k ₁ $/\$
26	6, 25	mpbiran2 885	. . . . . . . . . . . . . . . . . . 19 ₁ _k ₁
27		snelpw1 4147	. . . . . . . . . . . . . . . . . . 19 ₁
28		vex 2863	. . . . . . . . . . . . . . . . . . . 20
29		elequ2 1715	. . . . . . . . . . . . . . . . . . . 20
30	28, 29	elab 2986	. . . . . . . . . . . . . . . . . . 19
31	26, 27, 30	3bitri 262	. . . . . . . . . . . . . . . . . 18 ₁ _k
32	28, 6	elssetk 4271	. . . . . . . . . . . . . . . . . 18 S_k
33	31, 32	anbi12i 678	. . . . . . . . . . . . . . . . 17 ₁ _k $/\$ S_k $/\$
34	23, 24, 33	3bitri 262	. . . . . . . . . . . . . . . 16 $/\$ ₁ _k S_k $/\$
35	34	exbii 1582	. . . . . . . . . . . . . . 15 $/\$ ₁ _k S_k $/\$
36	11, 19, 35	3bitri 262	. . . . . . . . . . . . . 14 ₁ _k S_k _k1_c $/\$
37		snelpw1 4147	. . . . . . . . . . . . . 14 ₁ ₁ _k S_k _k1_c ₁ _k S_k _k1_c
38		eluni 3895	. . . . . . . . . . . . . 14 $/\$
39	36, 37, 38	3bitr4i 268	. . . . . . . . . . . . 13 ₁ ₁ _k S_k _k1_c
40	10, 39	xchbinx 301	. . . . . . . . . . . 12 ∼ ₁ ₁ _k S_k _k1_c
41	1, 7	opkelxpk 4249	. . . . . . . . . . . . 13 ∼ ₁ ₁ _k S_k _k1_c _k ∼ ₁ ₁ _k S_k _k1_c $/\$
42	7, 41	mpbiran2 885	. . . . . . . . . . . 12 ∼ ₁ ₁ _k S_k _k1_c _k ∼ ₁ ₁ _k S_k _k1_c
43		vex 2863	. . . . . . . . . . . . 13
44	43	elcompl 3226	. . . . . . . . . . . 12 ∼
45	40, 42, 44	3bitr4i 268	. . . . . . . . . . 11 ∼ ₁ ₁ _k S_k _k1_c _k ∼
46		eqabb 2459	. . . . . . . . . . . . . . 15
47	46	anbi1i 676	. . . . . . . . . . . . . 14 $/\$ $/\$
48	47	exbii 1582	. . . . . . . . . . . . 13 $/\$ $/\$
49		df-clel 2349	. . . . . . . . . . . . 13 $/\$
50		opkex 4114	. . . . . . . . . . . . . . 15
51	50	elimak 4260	. . . . . . . . . . . . . 14 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
52		elpw121c 4149	. . . . . . . . . . . . . . . . . 18 ₁ ₁ 1_c
53	52	anbi1i 676	. . . . . . . . . . . . . . . . 17 ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
54		19.41v 1901	. . . . . . . . . . . . . . . . 17 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
55	53, 54	bitr4i 243	. . . . . . . . . . . . . . . 16 ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
56	55	exbii 1582	. . . . . . . . . . . . . . 15 ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
57		df-rex 2621	. . . . . . . . . . . . . . 15 ₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
58		excom 1741	. . . . . . . . . . . . . . 15 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
59	56, 57, 58	3bitr4i 268	. . . . . . . . . . . . . 14 ₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
60		snex 4112	. . . . . . . . . . . . . . . . 17
61		opkeq1 4060	. . . . . . . . . . . . . . . . . 18
62	61	eleq1d 2419	. . . . . . . . . . . . . . . . 17 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
63	60, 62	ceqsexv 2895	. . . . . . . . . . . . . . . 16 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
64		elin 3220	. . . . . . . . . . . . . . . 16 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins2_k S_k
65		snex 4112	. . . . . . . . . . . . . . . . . . 19
66	65, 1, 7	otkelins3k 4257	. . . . . . . . . . . . . . . . . 18 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
67		vex 2863	. . . . . . . . . . . . . . . . . . 19
68	67, 6	opksnelsik 4266	. . . . . . . . . . . . . . . . . 18 SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
69		opkex 4114	. . . . . . . . . . . . . . . . . . . . . 22
70	69	elimak 4260	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c ₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
71		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ₁ ₁ 1_c
72	71	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . 24 ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
73		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
74	72, 73	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . 23 ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
75	74	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
76		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
77		excom 1741	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
78	75, 76, 77	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
79		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24
80		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . 25
81	80	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
82	79, 81	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
83		elsymdif 3224	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
84	20, 67, 6	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3_k S_k S_k
85	28, 67	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 S_k
86	84, 85	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3_k S_k
87		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
88	87	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
89		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ₁ ₁ 1_c
90	89	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
91		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
92	90, 91	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
93	92	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
94		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
95		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
96	93, 94, 95	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
97		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
99	98	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
100	97, 99	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
101		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
102		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
103	102, 20, 6	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins2_k S_k S_k
104		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104, 6	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 S_k
106	103, 105	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins2_k S_k
107	102, 20, 6	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
108	104, 28	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
109		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
111		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
112	111	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
113	111	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k S_k Ins3_k S_k _k
114	52	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k S_k _k $/\$ Ins2_k S_k Ins3_k S_k _k
115		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ Ins2_k S_k Ins3_k S_k _k $/\$ Ins2_k S_k Ins3_k S_k _k
116	114, 115	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k S_k _k $/\$ Ins2_k S_k Ins3_k S_k _k
117	116	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k S_k _k $/\$ Ins2_k S_k Ins3_k S_k _k
118		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ₁ ₁ 1_c Ins2_k S_k Ins3_k S_k _k ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k S_k _k
119		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Ins2_k S_k Ins3_k S_k _k $/\$ Ins2_k S_k Ins3_k S_k _k
120	117, 118, 119	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ₁ ₁ 1_c Ins2_k S_k Ins3_k S_k _k $/\$ Ins2_k S_k Ins3_k S_k _k
121		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
122	121	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2_k S_k Ins3_k S_k _k Ins2_k S_k Ins3_k S_k _k
123	60, 122	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ Ins2_k S_k Ins3_k S_k _k Ins2_k S_k Ins3_k S_k _k
124		elsymdif 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2_k S_k Ins3_k S_k _k Ins2_k S_k Ins3_k S_k _k
125	65, 104, 28	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2_k S_k S_k
126	67, 28	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 S_k
127	125, 126	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2_k S_k
128	65, 104, 28	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins3_k S_k _k S_k _k
129	67, 104	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 S_k
130	65	elsnc 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
131	67	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
132	130, 131	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
133	65, 104	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 _k $/\$
134	104, 133	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 _k
135	67	elsnc 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
136	132, 134, 135	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 _k
137	129, 136	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 S_k $\/$ _k $\/$
138		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 S_k _k S_k $\/$ _k
139		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\/$
140	137, 138, 139	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 S_k _k
141	128, 140	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins3_k S_k _k
142	127, 141	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2_k S_k Ins3_k S_k _k
143	124, 142	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2_k S_k Ins3_k S_k _k
144	123, 143	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Ins2_k S_k Ins3_k S_k _k
145	144	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Ins2_k S_k Ins3_k S_k _k
146	113, 120, 145	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
147	112, 146	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
148	109, 110, 147	3bitr4ri 269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
149	107, 108, 148	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
150	106, 149	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$
151	100, 101, 150	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$
152	151	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c $/\$
153	88, 96, 152	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c $/\$
154	20, 67, 6	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
155		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
156	153, 154, 155	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
157	86, 156	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
158	83, 157	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
159	82, 158	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
160	159	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
161	70, 78, 160	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
162	161	notbii 287	. . . . . . . . . . . . . . . . . . 19 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
163	69	elcompl 3226	. . . . . . . . . . . . . . . . . . 19 ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
164		alex 1572	. . . . . . . . . . . . . . . . . . 19
165	162, 163, 164	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
166	66, 68, 165	3bitri 262	. . . . . . . . . . . . . . . . 17 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
167	65, 1, 7	otkelins2k 4256	. . . . . . . . . . . . . . . . . 18 Ins2_k S_k S_k
168	67, 7	elssetk 4271	. . . . . . . . . . . . . . . . . 18 S_k
169	167, 168	bitri 240	. . . . . . . . . . . . . . . . 17 Ins2_k S_k
170	166, 169	anbi12i 678	. . . . . . . . . . . . . . . 16 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c $/\$ Ins2_k S_k $/\$
171	63, 64, 170	3bitri 262	. . . . . . . . . . . . . . 15 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$
172	171	exbii 1582	. . . . . . . . . . . . . 14 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k $/\$
173	51, 59, 172	3bitri 262	. . . . . . . . . . . . 13 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$
174	48, 49, 173	3bitr4ri 269	. . . . . . . . . . . 12 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
175	174	notbii 287	. . . . . . . . . . 11 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
176	45, 175	anbi12i 678	. . . . . . . . . 10 ∼ ₁ ₁ _k S_k _k1_c _k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ∼ $/\$
177		annim 414	. . . . . . . . . 10 ∼ $/\$ ∼
178	9, 176, 177	3bitri 262	. . . . . . . . 9 ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ∼
179	8, 178	anbi12i 678	. . . . . . . 8 S_k $/\$ ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ ∼
180	4, 5, 179	3bitri 262	. . . . . . 7 $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ ∼
181	180	exbii 1582	. . . . . 6 $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ ∼
182	7	elimak 4260	. . . . . . 7 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c 1_c S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
183		el1c 4140	. . . . . . . . . . 11 1_c
184	183	anbi1i 676	. . . . . . . . . 10 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
185		19.41v 1901	. . . . . . . . . 10 $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
186	184, 185	bitr4i 243	. . . . . . . . 9 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
187	186	exbii 1582	. . . . . . . 8 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
188		df-rex 2621	. . . . . . . 8 1_c S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
189		excom 1741	. . . . . . . 8 $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
190	187, 188, 189	3bitr4i 268	. . . . . . 7 1_c S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
191	182, 190	bitri 240	. . . . . 6 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c $/\$ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
192		df-rex 2621	. . . . . 6 ∼ $/\$ ∼
193	181, 191, 192	3bitr4i 268	. . . . 5 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c ∼
194	193	notbii 287	. . . 4 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c ∼
195	7	elcompl 3226	. . . 4 ∼ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c
196		dfral2 2627	. . . 4 ∼ ∼
197	194, 195, 196	3bitr4i 268	. . 3 ∼ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c ∼
198	197	eqabi 2465	. 2 ∼ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c ∼
199		ssetkex 4295	. . . . 5 S_k
200		setswithex 4323	. . . . . . . . . . . . 13
201	200	pw1ex 4304	. . . . . . . . . . . 12 ₁
202		vvex 4110	. . . . . . . . . . . 12
203	201, 202	xpkex 4290	. . . . . . . . . . 11 ₁ _k
204	203, 199	inex 4106	. . . . . . . . . 10 ₁ _k S_k
205		1cex 4143	. . . . . . . . . 10 1_c
206	204, 205	imakex 4301	. . . . . . . . 9 ₁ _k S_k _k1_c
207	206	pw1ex 4304	. . . . . . . 8 ₁ ₁ _k S_k _k1_c
208	207	complex 4105	. . . . . . 7 ∼ ₁ ₁ _k S_k _k1_c
209	208, 202	xpkex 4290	. . . . . 6 ∼ ₁ ₁ _k S_k _k1_c _k
210	199	ins3kex 4309	. . . . . . . . . . . . 13 Ins3_k S_k
211	199	ins2kex 4308	. . . . . . . . . . . . . . . 16 Ins2_k S_k
212		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24
213	212, 202	xpkex 4290	. . . . . . . . . . . . . . . . . . . . . . 23 _k
214	199, 213	unex 4107	. . . . . . . . . . . . . . . . . . . . . 22 S_k _k
215	214	ins3kex 4309	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k S_k _k
216	211, 215	symdifex 4109	. . . . . . . . . . . . . . . . . . . 20 Ins2_k S_k Ins3_k S_k _k
217	205	pw1ex 4304	. . . . . . . . . . . . . . . . . . . . 21 ₁ 1_c
218	217	pw1ex 4304	. . . . . . . . . . . . . . . . . . . 20 ₁ ₁ 1_c
219	216, 218	imakex 4301	. . . . . . . . . . . . . . . . . . 19 Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
220	219	complex 4105	. . . . . . . . . . . . . . . . . 18 ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
221	220	sikex 4298	. . . . . . . . . . . . . . . . 17 SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
222	221	ins3kex 4309	. . . . . . . . . . . . . . . 16 Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
223	211, 222	inex 4106	. . . . . . . . . . . . . . 15 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c
224	223, 218	imakex 4301	. . . . . . . . . . . . . 14 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
225	224	ins2kex 4308	. . . . . . . . . . . . 13 Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
226	210, 225	symdifex 4109	. . . . . . . . . . . 12 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c
227	226, 218	imakex 4301	. . . . . . . . . . 11 Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
228	227	complex 4105	. . . . . . . . . 10 ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
229	228	sikex 4298	. . . . . . . . 9 SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
230	229	ins3kex 4309	. . . . . . . 8 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c
231	230, 211	inex 4106	. . . . . . 7 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k
232	231, 218	imakex 4301	. . . . . 6 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
233	209, 232	difex 4108	. . . . 5 ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
234	199, 233	inex 4106	. . . 4 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
235	234, 205	imakex 4301	. . 3 S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c
236	235	complex 4105	. 2 ∼ S_k ∼ ₁ ₁ _k S_k _k1_c _k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k S_k _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k1_c
237	198, 236	eqeltrri 2424	1 ∼

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 176 $\/$ wo 357 $/\$ wa 358

wal 1540

wex 1541

wceq 1642

wcel 1710

cab 2339

wral 2615

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cun 3208

cin 3209

csymdif 3210

csn 3738

cuni 3892

copk 4058 1_cc1c 4135

₁ cpw1 4136

_k cxpk 4175 Ins2_k cins2k 4177 Ins3_k cins3k 4178

_kcimak 4180 SI_k csik 4182 S_k cssetk 4184

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-14 1714 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-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-p6 4192 df-sik 4193 df-ssetk 4194

This theorem is referenced by: nnadjoin 4521

W3C validator