nchoicelem11 - New Foundations Explorer

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

Theorem nchoicelem11 6300

Description: Lemma for nchoice 6309. Set up stratification for nchoicelem12 6301. (Contributed by SF, 18-Mar-2015.)

**Assertion**
Ref	Expression
nchoicelem11	⊢ {t ∣ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn )} ∈ V

Distinct variable group: t,m

Proof of Theorem nchoicelem11 Dummy variables a b u x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . 5 ⊢ t ∈ V
2	1	elcompl 3226	. . . 4 ⊢ (t ∈ ∼ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ↔ ¬ t ∈ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ))
3		elimapw13 4947	. . . . . . 7 ⊢ (t ∈ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ↔ ∃m ∈ NC ⟨{{{m}}}, t⟩ ∈ ((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)))
4		tccl 6161	. . . . . . . . . . . . . 14 ⊢ (m ∈ NC → T_c m ∈ NC )
5		spacval 6283	. . . . . . . . . . . . . 14 ⊢ ( T_c m ∈ NC → ( Sp_ac ‘ T_c m) = Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
6	4, 5	syl 15	. . . . . . . . . . . . 13 ⊢ (m ∈ NC → ( Sp_ac ‘ T_c m) = Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
7	6	nceqd 6111	. . . . . . . . . . . 12 ⊢ (m ∈ NC → Nc ( Sp_ac ‘ T_c m) = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
8	7	eqeq2d 2364	. . . . . . . . . . 11 ⊢ (m ∈ NC → (t = Nc ( Sp_ac ‘ T_c m) ↔ t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))
9		finnc 6244	. . . . . . . . . . . 12 ⊢ (( Sp_ac ‘m) ∈ Fin ↔ Nc ( Sp_ac ‘m) ∈ Nn )
10		spacval 6283	. . . . . . . . . . . . 13 ⊢ (m ∈ NC → ( Sp_ac ‘m) = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
11	10	eleq1d 2419	. . . . . . . . . . . 12 ⊢ (m ∈ NC → (( Sp_ac ‘m) ∈ Fin ↔ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ))
12	9, 11	syl5bbr 250	. . . . . . . . . . 11 ⊢ (m ∈ NC → ( Nc ( Sp_ac ‘m) ∈ Nn ↔ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ))
13	8, 12	imbi12d 311	. . . . . . . . . 10 ⊢ (m ∈ NC → ((t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ) ↔ (t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) → Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin )))
14	13	notbid 285	. . . . . . . . 9 ⊢ (m ∈ NC → (¬ (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ) ↔ ¬ (t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) → Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin )))
15		eldif 3222	. . . . . . . . . 10 ⊢ (⟨{{{m}}}, t⟩ ∈ ((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) ↔ (⟨{{{m}}}, t⟩ ∈ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∧ ¬ ⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)))
16		opelco 4885	. . . . . . . . . . . . . 14 ⊢ (⟨{{{m}}}, t⟩ ∈ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ↔ ∃a({{{m}}} SI SI TcFna ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
17		snex 4112	. . . . . . . . . . . . . . . . . . 19 ⊢ {{m}} ∈ V
18	17	brsnsi1 5776	. . . . . . . . . . . . . . . . . 18 ⊢ ({{{m}}} SI SI TcFna ↔ ∃b(a = {b} ∧ {{m}} SI TcFnb))
19	18	anbi1i 676	. . . . . . . . . . . . . . . . 17 ⊢ (({{{m}}} SI SI TcFna ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (∃b(a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
20		19.41v 1901	. . . . . . . . . . . . . . . . . 18 ⊢ (∃b((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (∃b(a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
21	20	bicomi 193	. . . . . . . . . . . . . . . . 17 ⊢ ((∃b(a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃b((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
22	19, 21	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ (({{{m}}} SI SI TcFna ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃b((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
23	22	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃a({{{m}}} SI SI TcFna ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃a∃b((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
24		excom 1741	. . . . . . . . . . . . . . . 16 ⊢ (∃a∃b((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃b∃a((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
25		anass 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (a = {b} ∧ ({{m}} SI TcFnb ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)))
26	25	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃a((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃a(a = {b} ∧ ({{m}} SI TcFnb ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)))
27		snex 4112	. . . . . . . . . . . . . . . . . . . 20 ⊢ {b} ∈ V
28		breq1 4643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (a = {b} → (a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t ↔ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
29	28	anbi2d 684	. . . . . . . . . . . . . . . . . . . 20 ⊢ (a = {b} → (({{m}} SI TcFnb ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)))
30	27, 29	ceqsexv 2895	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃a(a = {b} ∧ ({{m}} SI TcFnb ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)) ↔ ({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
31	26, 30	bitri 240	. . . . . . . . . . . . . . . . . 18 ⊢ (∃a((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
32	31	exbii 1582	. . . . . . . . . . . . . . . . 17 ⊢ (∃b∃a((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃b({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
33		snex 4112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {m} ∈ V
34	33	brsnsi1 5776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({{m}} SI TcFnb ↔ ∃u(b = {u} ∧ {m}TcFnu))
35	34	anbi1i 676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (∃u(b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
36		19.41v 1901	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃u((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (∃u(b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
37	35, 36	bitr4i 243	. . . . . . . . . . . . . . . . . . 19 ⊢ (({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
38	37	exbii 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (∃b({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃b∃u((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
39		excom 1741	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃b∃u((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u∃b((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
40		anass 630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (b = {u} ∧ ({m}TcFnu ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)))
41	40	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃b((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃b(b = {u} ∧ ({m}TcFnu ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)))
42		snex 4112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {u} ∈ V
43		sneq 3745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (b = {u} → {b} = {{u}})
44	43	breq1d 4650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (b = {u} → ({b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t ↔ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
45	44	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (b = {u} → (({m}TcFnu ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)))
46	42, 45	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃b(b = {u} ∧ ({m}TcFnu ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t)) ↔ ({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
47	41, 46	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃b((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
48	47	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃u∃b((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
49	39, 48	bitri 240	. . . . . . . . . . . . . . . . . 18 ⊢ (∃b∃u((b = {u} ∧ {m}TcFnu) ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
50	38, 49	bitri 240	. . . . . . . . . . . . . . . . 17 ⊢ (∃b({{m}} SI TcFnb ∧ {b}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
51	32, 50	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ (∃b∃a((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
52	24, 51	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (∃a∃b((a = {b} ∧ {{m}} SI TcFnb) ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
53	23, 52	bitri 240	. . . . . . . . . . . . . 14 ⊢ (∃a({{{m}}} SI SI TcFna ∧ a^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
54	16, 53	bitri 240	. . . . . . . . . . . . 13 ⊢ (⟨{{{m}}}, t⟩ ∈ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ↔ ∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t))
55		vex 2863	. . . . . . . . . . . . . . . 16 ⊢ m ∈ V
56	55	brtcfn 6247	. . . . . . . . . . . . . . 15 ⊢ ({m}TcFnu ↔ u = T_c m)
57		df-br 4641	. . . . . . . . . . . . . . . . 17 ⊢ ({{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t ↔ ⟨{{u}}, t⟩ ∈ ^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )))
58		opelcnv 4894	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨{{u}}, t⟩ ∈ ^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ↔ ⟨t, {{u}}⟩ ∈ (( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )))
59		elin 3220	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨t, {{u}}⟩ ∈ (( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ↔ (⟨t, {{u}}⟩ ∈ ( NC × V) ∧ ⟨t, {{u}}⟩ ∈ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )))
60		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {{u}} ∈ V
61		opelxp 4812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨t, {{u}}⟩ ∈ ( NC × V) ↔ (t ∈ NC ∧ {{u}} ∈ V))
62	60, 61	mpbiran2 885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨t, {{u}}⟩ ∈ ( NC × V) ↔ t ∈ NC )
63		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}) ↔ (b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}} ∧ t^◡ S b))
64	42	brsnsi2 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}} ↔ ∃a(b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}))
65	64	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}} ∧ t^◡ S b) ↔ (∃a(b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
66	63, 65	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}) ↔ (∃a(b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
67		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃a((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ (∃a(b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
68	66, 67	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}) ↔ ∃a((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
69	68	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃b(t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}) ↔ ∃b∃a((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
70		excom 1741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃b∃a((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ ∃a∃b((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
71	69, 70	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃b(t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}) ↔ ∃a∃b((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b))
72		anass 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ (b = {a} ∧ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S b)))
73	72	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃b((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ ∃b(b = {a} ∧ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S b)))
74		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {a} ∈ V
75		breq2 4644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (b = {a} → (t^◡ S b ↔ t^◡ S {a}))
76	75	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (b = {a} → ((a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S b) ↔ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S {a})))
77	74, 76	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃b(b = {a} ∧ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S b)) ↔ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S {a}))
78	73, 77	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃b((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S {a}))
79		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ↔ ⟨a, {u}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c))
80		spacvallem1 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))} ∈ V
81	80, 42	nchoicelem10 6299	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨a, {u}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ↔ a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
82	79, 81	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ↔ a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
83		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (t^◡ S {a} ↔ {a} S t)
84		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ a ∈ V
85	84, 1	brssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({a} S t ↔ a ∈ t)
86	83, 85	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t^◡ S {a} ↔ a ∈ t)
87	82, 86	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u} ∧ t^◡ S {a}) ↔ (a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ a ∈ t))
88	78, 87	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃b((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ (a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ a ∈ t))
89	88	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃a∃b((b = {a} ∧ a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){u}) ∧ t^◡ S b) ↔ ∃a(a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ a ∈ t))
90	71, 89	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃b(t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}) ↔ ∃a(a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ a ∈ t))
91		opelco 4885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨t, {{u}}⟩ ∈ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ) ↔ ∃b(t^◡ S b ∧ b SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){{u}}))
92		df-clel 2349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t ↔ ∃a(a = Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ a ∈ t))
93	90, 91, 92	3bitr4i 268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨t, {{u}}⟩ ∈ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ) ↔ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t)
94	62, 93	anbi12i 678	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨t, {{u}}⟩ ∈ ( NC × V) ∧ ⟨t, {{u}}⟩ ∈ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ↔ (t ∈ NC ∧ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t))
95	59, 94	bitri 240	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨t, {{u}}⟩ ∈ (( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ↔ (t ∈ NC ∧ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t))
96	58, 95	bitri 240	. . . . . . . . . . . . . . . . 17 ⊢ (⟨{{u}}, t⟩ ∈ ^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ↔ (t ∈ NC ∧ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t))
97	57, 96	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ ({{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t ↔ (t ∈ NC ∧ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t))
98	42, 80	clos1ex 5877	. . . . . . . . . . . . . . . . 17 ⊢ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ V
99	98	eqnc2 6130	. . . . . . . . . . . . . . . 16 ⊢ (t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ↔ (t ∈ NC ∧ Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ t))
100	97, 99	bitr4i 243	. . . . . . . . . . . . . . 15 ⊢ ({{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t ↔ t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
101	56, 100	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ (({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ (u = T_c m ∧ t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))
102	101	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃u({m}TcFnu ∧ {{u}}^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ))t) ↔ ∃u(u = T_c m ∧ t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))
103	54, 102	bitri 240	. . . . . . . . . . . 12 ⊢ (⟨{{{m}}}, t⟩ ∈ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ↔ ∃u(u = T_c m ∧ t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))
104		tcex 6158	. . . . . . . . . . . . 13 ⊢ T_c m ∈ V
105		sneq 3745	. . . . . . . . . . . . . . . 16 ⊢ (u = T_c m → {u} = { T_c m})
106		clos1eq1 5875	. . . . . . . . . . . . . . . 16 ⊢ ({u} = { T_c m} → Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) = Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
107	105, 106	syl 15	. . . . . . . . . . . . . . 15 ⊢ (u = T_c m → Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) = Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
108	107	nceqd 6111	. . . . . . . . . . . . . 14 ⊢ (u = T_c m → Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
109	108	eqeq2d 2364	. . . . . . . . . . . . 13 ⊢ (u = T_c m → (t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ↔ t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))
110	104, 109	ceqsexv 2895	. . . . . . . . . . . 12 ⊢ (∃u(u = T_c m ∧ t = Nc Clos1 ({u}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})) ↔ t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
111	103, 110	bitri 240	. . . . . . . . . . 11 ⊢ (⟨{{{m}}}, t⟩ ∈ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ↔ t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
112		df-br 4641	. . . . . . . . . . . . . . 15 ⊢ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m} ↔ ⟨a, {m}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c))
113	80, 33	nchoicelem10 6299	. . . . . . . . . . . . . . 15 ⊢ (⟨a, {m}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ↔ a = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
114	112, 113	bitri 240	. . . . . . . . . . . . . 14 ⊢ (a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m} ↔ a = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
115	114	rexbii 2640	. . . . . . . . . . . . 13 ⊢ (∃a ∈ Fin a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m} ↔ ∃a ∈ Fin a = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
116		opelxp 4812	. . . . . . . . . . . . . . 15 ⊢ (⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V) ↔ ({{{m}}} ∈ ℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ∧ t ∈ V))
117	1, 116	mpbiran2 885	. . . . . . . . . . . . . 14 ⊢ (⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V) ↔ {{{m}}} ∈ ℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ))
118		snelpw1 4147	. . . . . . . . . . . . . . 15 ⊢ ({{{m}}} ∈ ℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ↔ {{m}} ∈ ℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ))
119		snelpw1 4147	. . . . . . . . . . . . . . . 16 ⊢ ({{m}} ∈ ℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ↔ {m} ∈ ( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ))
120		elima 4755	. . . . . . . . . . . . . . . 16 ⊢ ({m} ∈ ( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ↔ ∃a ∈ Fin a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m})
121	119, 120	bitri 240	. . . . . . . . . . . . . . 15 ⊢ ({{m}} ∈ ℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ↔ ∃a ∈ Fin a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m})
122	118, 121	bitri 240	. . . . . . . . . . . . . 14 ⊢ ({{{m}}} ∈ ℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ↔ ∃a ∈ Fin a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m})
123	117, 122	bitri 240	. . . . . . . . . . . . 13 ⊢ (⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V) ↔ ∃a ∈ Fin a ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c){m})
124		risset 2662	. . . . . . . . . . . . 13 ⊢ ( Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ↔ ∃a ∈ Fin a = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))
125	115, 123, 124	3bitr4i 268	. . . . . . . . . . . 12 ⊢ (⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V) ↔ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin )
126	125	notbii 287	. . . . . . . . . . 11 ⊢ (¬ ⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V) ↔ ¬ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin )
127	111, 126	anbi12i 678	. . . . . . . . . 10 ⊢ ((⟨{{{m}}}, t⟩ ∈ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∧ ¬ ⟨{{{m}}}, t⟩ ∈ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) ↔ (t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ ¬ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ))
128		annim 414	. . . . . . . . . 10 ⊢ ((t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∧ ¬ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ) ↔ ¬ (t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) → Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ))
129	15, 127, 128	3bitri 262	. . . . . . . . 9 ⊢ (⟨{{{m}}}, t⟩ ∈ ((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) ↔ ¬ (t = Nc Clos1 ({ T_c m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) → Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ Fin ))
130	14, 129	syl6rbbr 255	. . . . . . . 8 ⊢ (m ∈ NC → (⟨{{{m}}}, t⟩ ∈ ((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) ↔ ¬ (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn )))
131	130	rexbiia 2648	. . . . . . 7 ⊢ (∃m ∈ NC ⟨{{{m}}}, t⟩ ∈ ((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) ↔ ∃m ∈ NC ¬ (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ))
132	3, 131	bitri 240	. . . . . 6 ⊢ (t ∈ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ↔ ∃m ∈ NC ¬ (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ))
133		rexnal 2626	. . . . . 6 ⊢ (∃m ∈ NC ¬ (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ) ↔ ¬ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ))
134	132, 133	bitr2i 241	. . . . 5 ⊢ (¬ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ) ↔ t ∈ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ))
135	134	con1bii 321	. . . 4 ⊢ (¬ t ∈ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ↔ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ))
136	2, 135	bitri 240	. . 3 ⊢ (t ∈ ∼ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ↔ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn ))
137	136	eqabi 2465	. 2 ⊢ ∼ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) = {t ∣ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn )}
138		ncsex 6112	. . . . . . . . 9 ⊢ NC ∈ V
139		vvex 4110	. . . . . . . . 9 ⊢ V ∈ V
140	138, 139	xpex 5116	. . . . . . . 8 ⊢ ( NC × V) ∈ V
141		ssetex 4745	. . . . . . . . . . . . . 14 ⊢ S ∈ V
142	141	ins3ex 5799	. . . . . . . . . . . . 13 ⊢ Ins3 S ∈ V
143	141	complex 4105	. . . . . . . . . . . . . . . . . 18 ⊢ ∼ S ∈ V
144	143	cnvex 5103	. . . . . . . . . . . . . . . . 17 ⊢ ^◡ ∼ S ∈ V
145	141	cnvex 5103	. . . . . . . . . . . . . . . . . 18 ⊢ ^◡ S ∈ V
146	80	imageex 5802	. . . . . . . . . . . . . . . . . . . 20 ⊢ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))} ∈ V
147	141, 146	coex 4751	. . . . . . . . . . . . . . . . . . 19 ⊢ ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ V
148	147	fixex 5790	. . . . . . . . . . . . . . . . . 18 ⊢ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}) ∈ V
149	145, 148	resex 5118	. . . . . . . . . . . . . . . . 17 ⊢ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})) ∈ V
150	144, 149	txpex 5786	. . . . . . . . . . . . . . . 16 ⊢ (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))) ∈ V
151	150	rnex 5108	. . . . . . . . . . . . . . 15 ⊢ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))) ∈ V
152	151	complex 4105	. . . . . . . . . . . . . 14 ⊢ ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))) ∈ V
153	152	ins2ex 5798	. . . . . . . . . . . . 13 ⊢ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))}))) ∈ V
154	142, 153	symdifex 4109	. . . . . . . . . . . 12 ⊢ ( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) ∈ V
155		1cex 4143	. . . . . . . . . . . 12 ⊢ 1_c ∈ V
156	154, 155	imaex 4748	. . . . . . . . . . 11 ⊢ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∈ V
157	156	complex 4105	. . . . . . . . . 10 ⊢ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∈ V
158	157	siex 4754	. . . . . . . . 9 ⊢ SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∈ V
159	158, 145	coex 4751	. . . . . . . 8 ⊢ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S ) ∈ V
160	140, 159	inex 4106	. . . . . . 7 ⊢ (( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∈ V
161	160	cnvex 5103	. . . . . 6 ⊢ ^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∈ V
162		tcfnex 6245	. . . . . . . 8 ⊢ TcFn ∈ V
163	162	siex 4754	. . . . . . 7 ⊢ SI TcFn ∈ V
164	163	siex 4754	. . . . . 6 ⊢ SI SI TcFn ∈ V
165	161, 164	coex 4751	. . . . 5 ⊢ (^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∈ V
166		finex 4398	. . . . . . . . 9 ⊢ Fin ∈ V
167	157, 166	imaex 4748	. . . . . . . 8 ⊢ ( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ∈ V
168	167	pw1ex 4304	. . . . . . 7 ⊢ ℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ∈ V
169	168	pw1ex 4304	. . . . . 6 ⊢ ℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) ∈ V
170	169, 139	xpex 5116	. . . . 5 ⊢ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V) ∈ V
171	165, 170	difex 4108	. . . 4 ⊢ ((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) ∈ V
172	138	pw1ex 4304	. . . . . 6 ⊢ ℘₁ NC ∈ V
173	172	pw1ex 4304	. . . . 5 ⊢ ℘₁℘₁ NC ∈ V
174	173	pw1ex 4304	. . . 4 ⊢ ℘₁℘₁℘₁ NC ∈ V
175	171, 174	imaex 4748	. . 3 ⊢ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ∈ V
176	175	complex 4105	. 2 ⊢ ∼ (((^◡(( NC × V) ∩ ( SI ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) ∘ ^◡ S )) ∘ SI SI TcFn) ∖ (℘₁℘₁( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (^◡ ∼ S ⊗ (^◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_c ↑_c x))})))) “ 1_c) “ Fin ) × V)) “ ℘₁℘₁℘₁ NC ) ∈ V
177	137, 176	eqeltrri 2424	1 ⊢ {t ∣ ∀m ∈ NC (t = Nc ( Sp_ac ‘ T_c m) → Nc ( Sp_ac ‘m) ∈ Nn )} ∈ V

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 358 ∧ w3a 934 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∀wral 2615 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∩ cin 3209 ⊕ csymdif 3210 {csn 3738 1_cc1c 4135 ℘₁cpw1 4136 Nn cnnc 4374 Fin cfin 4377 ⟨cop 4562 {copab 4623 class class class wbr 4640 S csset 4720 SI csi 4721 ∘ ccom 4722 “ cima 4723 × cxp 4771 ^◡ccnv 4772 ran crn 4774 ↾ cres 4775 ‘cfv 4782 (class class class)co 5526 ⊗ ctxp 5736 Fix cfix 5740 Ins2 cins2 5750 Ins3 cins3 5752 Imagecimage 5754 Clos1 cclos1 5873 NC cncs 6089 Nc cnc 6092 T_c ctc 6094 2_cc2c 6095 ↑_c cce 6097 TcFnctcfn 6098 Sp_ac cspac 6274

This proof depends on 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-13 1712 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 proof depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 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-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-evenfin 4445 df-oddfin 4446 df-sfin 4447 df-spfin 4448 df-phi 4566 df-op 4567 df-proj1 4568 df-proj2 4569 df-opab 4624 df-br 4641 df-1st 4724 df-swap 4725 df-sset 4726 df-co 4727 df-ima 4728 df-si 4729 df-id 4768 df-xp 4785 df-cnv 4786 df-rn 4787 df-dm 4788 df-res 4789 df-fun 4790 df-fn 4791 df-f 4792 df-f1 4793 df-fo 4794 df-f1o 4795 df-fv 4796 df-2nd 4798 df-ov 5527 df-oprab 5529 df-mpt 5653 df-mpt2 5655 df-txp 5737 df-fix 5741 df-ins2 5751 df-ins3 5753 df-image 5755 df-ins4 5757 df-si3 5759 df-funs 5761 df-fns 5763 df-pw1fn 5767 df-fullfun 5769 df-clos1 5874 df-trans 5900 df-sym 5909 df-er 5910 df-ec 5948 df-qs 5952 df-map 6002 df-en 6030 df-ncs 6099 df-nc 6102 df-tc 6104 df-2c 6105 df-ce 6107 df-tcfn 6108 df-spac 6275

This theorem is used by: nchoicelem12 6301

W3C validator