srelk - New Foundations Explorer

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

Theorem srelk 4525

Description: Binary relationship form of the S_fin relationship. (Contributed by SF, 23-Jan-2015.)

**Hypotheses**
Ref	Expression
srelk.1
srelk.2

**Assertion**
Ref	Expression
srelk	Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin

Proof of Theorem srelk Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		srelk.1	. . . . 5
2		srelk.2	. . . . 5
3	1, 2	opkelxpk 4249	. . . 4 Nn _k Nn Nn $/\$ Nn
4		opkex 4114	. . . . . 6
5	4	elimak 4260	. . . . 5 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁ ₁ ₁ 1_c Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
6		elpw131c 4150	. . . . . . . . 9 ₁ ₁ ₁ 1_c
7	6	anbi1i 676	. . . . . . . 8 ₁ ₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
8		19.41v 1901	. . . . . . . 8 $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
9	7, 8	bitr4i 243	. . . . . . 7 ₁ ₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
10	9	exbii 1582	. . . . . 6 ₁ ₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
11		df-rex 2621	. . . . . 6 ₁ ₁ ₁ 1_c Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ ₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
12		excom 1741	. . . . . 6 $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
13	10, 11, 12	3bitr4i 268	. . . . 5 ₁ ₁ ₁ 1_c Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
14		snex 4112	. . . . . . . 8
15		opkeq1 4060	. . . . . . . . 9
16	15	eleq1d 2419	. . . . . . . 8 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
17	14, 16	ceqsexv 2895	. . . . . . 7 $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
18		elin 3220	. . . . . . 7 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
19		opkex 4114	. . . . . . . . . . 11
20	19	elimak 4260	. . . . . . . . . 10 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
21		elpw121c 4149	. . . . . . . . . . . . . 14 ₁ ₁ 1_c
22	21	anbi1i 676	. . . . . . . . . . . . 13 ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
23		19.41v 1901	. . . . . . . . . . . . 13 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
24	22, 23	bitr4i 243	. . . . . . . . . . . 12 ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
25	24	exbii 1582	. . . . . . . . . . 11 ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
26		df-rex 2621	. . . . . . . . . . 11 ₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k ₁ ₁ 1_c $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
27		excom 1741	. . . . . . . . . . 11 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
28	25, 26, 27	3bitr4i 268	. . . . . . . . . 10 ₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
29		snex 4112	. . . . . . . . . . . . 13
30		opkeq1 4060	. . . . . . . . . . . . . 14
31	30	eleq1d 2419	. . . . . . . . . . . . 13 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
32	29, 31	ceqsexv 2895	. . . . . . . . . . . 12 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k
33		elin 3220	. . . . . . . . . . . 12 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins2_k S_k
34		snex 4112	. . . . . . . . . . . . . . 15
35		snex 4112	. . . . . . . . . . . . . . 15
36	34, 35, 1	otkelins3k 4257	. . . . . . . . . . . . . 14 Ins3_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
37		vex 2863	. . . . . . . . . . . . . . 15
38		snex 4112	. . . . . . . . . . . . . . 15
39	37, 38	opksnelsik 4266	. . . . . . . . . . . . . 14 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
40		vex 2863	. . . . . . . . . . . . . . 15
41	37, 40	eqpw1relk 4480	. . . . . . . . . . . . . 14 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
42	36, 39, 41	3bitri 262	. . . . . . . . . . . . 13 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c ₁
43	34, 35, 1	otkelins2k 4256	. . . . . . . . . . . . . 14 Ins2_k S_k S_k
44	37, 1	elssetk 4271	. . . . . . . . . . . . . 14 S_k
45	43, 44	bitri 240	. . . . . . . . . . . . 13 Ins2_k S_k
46	42, 45	anbi12i 678	. . . . . . . . . . . 12 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c $/\$ Ins2_k S_k ₁ $/\$
47	32, 33, 46	3bitri 262	. . . . . . . . . . 11 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k ₁ $/\$
48	47	exbii 1582	. . . . . . . . . 10 $/\$ Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k ₁ $/\$
49	20, 28, 48	3bitri 262	. . . . . . . . 9 Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ $/\$
50	35, 1, 2	otkelins3k 4257	. . . . . . . . 9 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
51		df-clel 2349	. . . . . . . . 9 ₁ ₁ $/\$
52	49, 50, 51	3bitr4i 268	. . . . . . . 8 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁
53		opkex 4114	. . . . . . . . . . 11
54	53	elimak 4260	. . . . . . . . . 10 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
55	21	anbi1i 676	. . . . . . . . . . . . 13 ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
56		19.41v 1901	. . . . . . . . . . . . 13 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
57	55, 56	bitr4i 243	. . . . . . . . . . . 12 ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
58	57	exbii 1582	. . . . . . . . . . 11 ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
59		df-rex 2621	. . . . . . . . . . 11 ₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k ₁ ₁ 1_c $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
60		excom 1741	. . . . . . . . . . 11 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
61	58, 59, 60	3bitr4i 268	. . . . . . . . . 10 ₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
62		opkeq1 4060	. . . . . . . . . . . . . 14
63	62	eleq1d 2419	. . . . . . . . . . . . 13 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
64	29, 63	ceqsexv 2895	. . . . . . . . . . . 12 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k
65		elin 3220	. . . . . . . . . . . 12 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c $/\$ Ins2_k S_k
66	34, 35, 2	otkelins3k 4257	. . . . . . . . . . . . . 14 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
67	37, 38	opksnelsik 4266	. . . . . . . . . . . . . 14 SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
68		opkex 4114	. . . . . . . . . . . . . . . . . . 19
69	68	elimak 4260	. . . . . . . . . . . . . . . . . 18 Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k S_k
70		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . 22 ₁ ₁ 1_c
71	70	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k SI_k S_k $/\$ Ins3_k S_k Ins2_k SI_k S_k
72		19.41v 1901	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Ins3_k S_k Ins2_k SI_k S_k $/\$ Ins3_k S_k Ins2_k SI_k S_k
73	71, 72	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k SI_k S_k $/\$ Ins3_k S_k Ins2_k SI_k S_k
74	73	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k SI_k S_k $/\$ Ins3_k S_k Ins2_k SI_k S_k
75		df-rex 2621	. . . . . . . . . . . . . . . . . . 19 ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k S_k ₁ ₁ 1_c $/\$ Ins3_k S_k Ins2_k SI_k S_k
76		excom 1741	. . . . . . . . . . . . . . . . . . 19 $/\$ Ins3_k S_k Ins2_k SI_k S_k $/\$ Ins3_k S_k Ins2_k SI_k S_k
77	74, 75, 76	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k S_k $/\$ Ins3_k S_k Ins2_k SI_k S_k
78		snex 4112	. . . . . . . . . . . . . . . . . . . . 21
79		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22
80	79	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k S_k Ins2_k SI_k S_k Ins3_k S_k Ins2_k SI_k S_k
81	78, 80	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . 20 $/\$ Ins3_k S_k Ins2_k SI_k S_k Ins3_k S_k Ins2_k SI_k S_k
82		elsymdif 3224	. . . . . . . . . . . . . . . . . . . 20 Ins3_k S_k Ins2_k SI_k S_k Ins3_k S_k Ins2_k SI_k S_k
83		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24
84	83, 37, 38	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k S_k S_k
85		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24
86	85, 37	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . 23 S_k
87	84, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 Ins3_k S_k
88	83, 37, 38	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2_k SI_k S_k SI_k S_k
89	85, 40	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . 23 SI_k S_k S_k
90		opkelssetkg 4269	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ S_k
91	85, 40, 90	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . 23 S_k
92	88, 89, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 Ins2_k SI_k S_k
93	87, 92	bibi12i 306	. . . . . . . . . . . . . . . . . . . . 21 Ins3_k S_k Ins2_k SI_k S_k
94	93	notbii 287	. . . . . . . . . . . . . . . . . . . 20 Ins3_k S_k Ins2_k SI_k S_k
95	81, 82, 94	3bitri 262	. . . . . . . . . . . . . . . . . . 19 $/\$ Ins3_k S_k Ins2_k SI_k S_k
96	95	exbii 1582	. . . . . . . . . . . . . . . . . 18 $/\$ Ins3_k S_k Ins2_k SI_k S_k
97	69, 77, 96	3bitri 262	. . . . . . . . . . . . . . . . 17 Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
98	97	notbii 287	. . . . . . . . . . . . . . . 16 Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
99	68	elcompl 3226	. . . . . . . . . . . . . . . 16 ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
100		alex 1572	. . . . . . . . . . . . . . . 16
101	98, 99, 100	3bitr4i 268	. . . . . . . . . . . . . . 15 ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
102		df-pw 3725	. . . . . . . . . . . . . . . . 17
103	102	eqeq2i 2363	. . . . . . . . . . . . . . . 16
104		abeq2 2459	. . . . . . . . . . . . . . . 16
105	103, 104	bitri 240	. . . . . . . . . . . . . . 15
106	101, 105	bitr4i 243	. . . . . . . . . . . . . 14 ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
107	66, 67, 106	3bitri 262	. . . . . . . . . . . . 13 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c
108	34, 35, 2	otkelins2k 4256	. . . . . . . . . . . . . 14 Ins2_k S_k S_k
109	37, 2	elssetk 4271	. . . . . . . . . . . . . 14 S_k
110	108, 109	bitri 240	. . . . . . . . . . . . 13 Ins2_k S_k
111	107, 110	anbi12i 678	. . . . . . . . . . . 12 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c $/\$ Ins2_k S_k $/\$
112	64, 65, 111	3bitri 262	. . . . . . . . . . 11 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$
113	112	exbii 1582	. . . . . . . . . 10 $/\$ Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k $/\$
114	54, 61, 113	3bitri 262	. . . . . . . . 9 Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$
115	35, 1, 2	otkelins2k 4256	. . . . . . . . 9 Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
116		df-clel 2349	. . . . . . . . 9 $/\$
117	114, 115, 116	3bitr4i 268	. . . . . . . 8 Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c
118	52, 117	anbi12i 678	. . . . . . 7 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c $/\$ Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ $/\$
119	17, 18, 118	3bitri 262	. . . . . 6 $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ $/\$
120	119	exbii 1582	. . . . 5 $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c ₁ $/\$
121	5, 13, 120	3bitri 262	. . . 4 Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c ₁ $/\$
122	3, 121	anbi12i 678	. . 3 Nn _k Nn $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ Nn $/\$ ₁ $/\$
123		df-3an 936	. . 3 Nn $/\$ Nn $/\$ ₁ $/\$ Nn $/\$ Nn $/\$ ₁ $/\$
124	122, 123	bitr4i 243	. 2 Nn _k Nn $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn $/\$ Nn $/\$ ₁ $/\$
125		elin 3220	. 2 Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn _k Nn $/\$ Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
126		df-sfin 4447	. 2 S_fin Nn $/\$ Nn $/\$ ₁ $/\$
127	124, 125, 126	3bitr4i 268	1 Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176 $/\$ wa 358 $/\$ w3a 934

wal 1540

wex 1541

wceq 1642

wcel 1710

cab 2339

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cin 3209

csymdif 3210

wss 3258

cpw 3723

csn 3738

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 Nn cnnc 4374 S_fin wsfin 4439

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-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-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-pw 3725 df-sn 3742 df-pr 3743 df-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-sik 4193 df-ssetk 4194 df-sfin 4447

This theorem is referenced by: sfintfinlem1 4532 spfinex 4538

W3C validator