srelk - New Foundations Explorer

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

Theorem srelk 4524

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 4248	. . . 4 Nn _k Nn Nn $/\$ Nn
4		opkex 4113	. . . . . 6
5	4	elimak 4259	. . . . 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 4149	. . . . . . . . 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 2620	. . . . . 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 4111	. . . . . . . 8
15		opkeq1 4059	. . . . . . . . 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 2894	. . . . . . 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 3219	. . . . . . 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 4113	. . . . . . . . . . 11
20	19	elimak 4259	. . . . . . . . . 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 4148	. . . . . . . . . . . . . 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 2620	. . . . . . . . . . 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 4111	. . . . . . . . . . . . 13
30		opkeq1 4059	. . . . . . . . . . . . . 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 2894	. . . . . . . . . . . 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 3219	. . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . 15
35		snex 4111	. . . . . . . . . . . . . . 15
36	34, 35, 1	otkelins3k 4256	. . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . 15
38		snex 4111	. . . . . . . . . . . . . . 15
39	37, 38	opksnelsik 4265	. . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . 15
41	37, 40	eqpw1relk 4479	. . . . . . . . . . . . . 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 4255	. . . . . . . . . . . . . 14 Ins2_k S_k S_k
44	37, 1	elssetk 4270	. . . . . . . . . . . . . 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 4256	. . . . . . . . 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 4113	. . . . . . . . . . 11
54	53	elimak 4259	. . . . . . . . . 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 2620	. . . . . . . . . . 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 4059	. . . . . . . . . . . . . 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 2894	. . . . . . . . . . . 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 3219	. . . . . . . . . . . 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 4256	. . . . . . . . . . . . . 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 4265	. . . . . . . . . . . . . 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 4113	. . . . . . . . . . . . . . . . . . 19
69	68	elimak 4259	. . . . . . . . . . . . . . . . . 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 4148	. . . . . . . . . . . . . . . . . . . . . 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 2620	. . . . . . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . . . . . . . 21
79		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . . . . . . . . 20 $/\$ Ins3_k S_k Ins2_k SI_k S_k Ins3_k S_k Ins2_k SI_k S_k
82		elsymdif 3223	. . . . . . . . . . . . . . . . . . . 20 Ins3_k S_k Ins2_k SI_k S_k Ins3_k S_k Ins2_k SI_k S_k
83		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . 24
84	83, 37, 38	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3_k S_k S_k
85		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . 24
86	85, 37	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . 23 S_k
87	84, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 Ins3_k S_k
88	83, 37, 38	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2_k SI_k S_k SI_k S_k
89	85, 40	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . 23 SI_k S_k S_k
90		opkelssetkg 4268	. . . . . . . . . . . . . . . . . . . . . . . 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 3225	. . . . . . . . . . . . . . . 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 3724	. . . . . . . . . . . . . . . . 17
103	102	eqeq2i 2363	. . . . . . . . . . . . . . . 16
104		abeq2 2458	. . . . . . . . . . . . . . . 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 4255	. . . . . . . . . . . . . 14 Ins2_k S_k S_k
109	37, 2	elssetk 4270	. . . . . . . . . . . . . 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 4255	. . . . . . . . 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 3219	. 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 4446	. 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 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cin 3208

csymdif 3209

wss 3257

cpw 3722

csn 3737

copk 4057 1_cc1c 4134

₁ cpw1 4135

_k cxpk 4174 Ins2_k cins2k 4176 Ins3_k cins3k 4177

_kcimak 4179 SI_k csik 4181 S_k cssetk 4183 Nn cnnc 4373 S_fin wsfin 4438

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-sn 4087

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-pw 3724 df-sn 3741 df-pr 3742 df-opk 4058 df-1c 4136 df-pw1 4137 df-xpk 4185 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-sik 4192 df-ssetk 4193 df-sfin 4446

This theorem is referenced by: sfintfinlem1 4531 spfinex 4537

W3C validator