setconslem2 - New Foundations Explorer

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

Theorem setconslem2 4732

Description: Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)

**Hypotheses**
Ref	Expression
setconslem1.1
setconslem1.2

**Assertion**
Ref	Expression
setconslem2	Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c Phi 0_c

Distinct variable groups:

Proof of Theorem setconslem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpw121c 4148	. . . . . . 7 ₁ ₁ 1_c
2	1	anbi1i 676	. . . . . 6 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
3		19.41v 1901	. . . . . 6 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
4	2, 3	bitr4i 243	. . . . 5 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
5	4	exbii 1582	. . . 4 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
6		df-rex 2620	. . . 4 ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
7		excom 1741	. . . 4 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
8	5, 6, 7	3bitr4i 268	. . 3 ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
9		snex 4111	. . . . . 6
10		opkeq1 4059	. . . . . . 7
11	10	eleq1d 2419	. . . . . 6 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
12	9, 11	ceqsexv 2894	. . . . 5 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
13		elin 3219	. . . . 5 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
14		snex 4111	. . . . . . . 8
15		snex 4111	. . . . . . . 8
16		setconslem1.2	. . . . . . . 8
17	14, 15, 16	otkelins2k 4255	. . . . . . 7 Ins2_k S_k S_k
18		vex 2862	. . . . . . . 8
19	18, 16	elssetk 4270	. . . . . . 7 S_k
20	17, 19	bitri 240	. . . . . 6 Ins2_k S_k
21	14, 15, 16	otkelins3k 4256	. . . . . . 7 Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
22		setconslem1.1	. . . . . . . 8
23	18, 22	opksnelsik 4265	. . . . . . 7 SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
24		opkex 4113	. . . . . . . . . . . 12
25	24	elimak 4259	. . . . . . . . . . 11 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
26		elpw121c 4148	. . . . . . . . . . . . . . 15 ₁ ₁ 1_c
27	26	anbi1i 676	. . . . . . . . . . . . . 14 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
28		19.41v 1901	. . . . . . . . . . . . . 14 $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
29	27, 28	bitr4i 243	. . . . . . . . . . . . 13 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
30	29	exbii 1582	. . . . . . . . . . . 12 ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
31		df-rex 2620	. . . . . . . . . . . 12 ₁ ₁ 1_c Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k ₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
32		excom 1741	. . . . . . . . . . . 12 $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
33	30, 31, 32	3bitr4i 268	. . . . . . . . . . 11 ₁ ₁ 1_c Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
34	25, 33	bitri 240	. . . . . . . . . 10 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
35		snex 4111	. . . . . . . . . . . . 13
36		opkeq1 4059	. . . . . . . . . . . . . 14
37	36	eleq1d 2419	. . . . . . . . . . . . 13 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
38	35, 37	ceqsexv 2894	. . . . . . . . . . . 12 $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
39		elsymdif 3223	. . . . . . . . . . . . 13 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
40		snex 4111	. . . . . . . . . . . . . . . 16
41	40, 18, 22	otkelins2k 4255	. . . . . . . . . . . . . . 15 Ins2_k S_k S_k
42		vex 2862	. . . . . . . . . . . . . . . 16
43	42, 22	elssetk 4270	. . . . . . . . . . . . . . 15 S_k
44	41, 43	bitri 240	. . . . . . . . . . . . . 14 Ins2_k S_k
45	40, 18, 22	otkelins3k 4256	. . . . . . . . . . . . . . 15 Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k
46		vex 2862	. . . . . . . . . . . . . . . . . . . . . 22
47	42, 46	elssetk 4270	. . . . . . . . . . . . . . . . . . . . 21 S_k
48	18, 46	opkelimagek 4272	. . . . . . . . . . . . . . . . . . . . . 22 Image_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k
49	46, 18	opkelcnvk 4250	. . . . . . . . . . . . . . . . . . . . . 22 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Image_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k
50		dfphi2 4569	. . . . . . . . . . . . . . . . . . . . . . 23 Phi Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k
51	50	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . . . 22 Phi Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k
52	48, 49, 51	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . 21 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Phi
53	47, 52	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 S_k $/\$ _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k $/\$ Phi
54		ancom 437	. . . . . . . . . . . . . . . . . . . 20 $/\$ Phi Phi $/\$
55	53, 54	bitri 240	. . . . . . . . . . . . . . . . . . 19 S_k $/\$ _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Phi $/\$
56	55	exbii 1582	. . . . . . . . . . . . . . . . . 18 S_k $/\$ _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Phi $/\$
57	40, 18	opkelcok 4262	. . . . . . . . . . . . . . . . . 18 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k S_k $/\$ _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k
58	18	phiex 4572	. . . . . . . . . . . . . . . . . . 19 Phi
59	58	clel3 2977	. . . . . . . . . . . . . . . . . 18 Phi Phi $/\$
60	56, 57, 59	3bitr4i 268	. . . . . . . . . . . . . . . . 17 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k Phi
61	40, 18	opkelxpk 4248	. . . . . . . . . . . . . . . . . . 19 0_c _k 0_c $/\$
62	18, 61	mpbiran2 885	. . . . . . . . . . . . . . . . . 18 0_c _k 0_c
63	42	sneqb 3876	. . . . . . . . . . . . . . . . . . 19 0_c 0_c
64	40	elsnc 3756	. . . . . . . . . . . . . . . . . . 19 0_c 0_c
65	42	elsnc 3756	. . . . . . . . . . . . . . . . . . 19 0_c 0_c
66	63, 64, 65	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 0_c 0_c
67	62, 66	bitri 240	. . . . . . . . . . . . . . . . 17 0_c _k 0_c
68	60, 67	orbi12i 507	. . . . . . . . . . . . . . . 16 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k $\/$ 0_c _k Phi $\/$ 0_c
69		elun 3220	. . . . . . . . . . . . . . . 16 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k $\/$ 0_c _k
70		elun 3220	. . . . . . . . . . . . . . . 16 Phi 0_c Phi $\/$ 0_c
71	68, 69, 70	3bitr4i 268	. . . . . . . . . . . . . . 15 _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Phi 0_c
72	45, 71	bitri 240	. . . . . . . . . . . . . 14 Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Phi 0_c
73	44, 72	bibi12i 306	. . . . . . . . . . . . 13 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Phi 0_c
74	39, 73	xchbinx 301	. . . . . . . . . . . 12 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Phi 0_c
75	38, 74	bitri 240	. . . . . . . . . . 11 $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Phi 0_c
76	75	exbii 1582	. . . . . . . . . 10 $/\$ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k Phi 0_c
77		exnal 1574	. . . . . . . . . 10 Phi 0_c Phi 0_c
78	34, 76, 77	3bitri 262	. . . . . . . . 9 Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Phi 0_c
79	78	con2bii 322	. . . . . . . 8 Phi 0_c Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
80		dfcleq 2347	. . . . . . . 8 Phi 0_c Phi 0_c
81	24	elcompl 3225	. . . . . . . 8 ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
82	79, 80, 81	3bitr4ri 269	. . . . . . 7 ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Phi 0_c
83	21, 23, 82	3bitri 262	. . . . . 6 Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c Phi 0_c
84	20, 83	anbi12i 678	. . . . 5 Ins2_k S_k $/\$ Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Phi 0_c
85	12, 13, 84	3bitri 262	. . . 4 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Phi 0_c
86	85	exbii 1582	. . 3 $/\$ Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Phi 0_c
87	8, 86	bitri 240	. 2 ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c $/\$ Phi 0_c
88		opkex 4113	. . 3
89	88	elimak 4259	. 2 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c ₁ ₁ 1_c Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c
90		df-rex 2620	. 2 Phi 0_c $/\$ Phi 0_c
91	87, 89, 90	3bitr4i 268	1 Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c Phi 0_c

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wal 1540

wex 1541

wceq 1642

wcel 1710

wrex 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cun 3207

cin 3208

csymdif 3209

csn 3737

copk 4057 1_cc1c 4134

₁ cpw1 4135

_k cxpk 4174

_kccnvk 4175 Ins2_k cins2k 4176 Ins3_k cins3k 4177

_kcimak 4179

_k ccomk 4180 SI_k csik 4181 Image_kcimagek 4182 S_k cssetk 4183

_k cidk 4184 Nn cnnc 4373 0_cc0c 4374 Phi cphi 4562

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 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 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-sbc 3047 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-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-idk 4195 df-addc 4378 df-nnc 4379 df-phi 4565

This theorem is referenced by: setconslem3 4733 setconslem7 4737 dfswap2 4741

W3C validator