Theorem nchoicelem16 6305

Description: Lemma for nchoice 6309. Set up stratification for nchoicelem17 6306. (Contributed by SF, 19-Mar-2015.)

Assertion

Ref	Expression
nchoicelem16	⊢ {t ∣ ( ≤c We NC → ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))} ∈ V

Distinct variable group:   t,m

Proof of Theorem nchoicelem16

Dummy variables n u v x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unab 3522	. . 3 ⊢ ({t ∣ ¬ ≤c We NC } ∪ {t ∣ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))}) = {t ∣ (¬ ≤c We NC ∨ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))}
2		elima3 4757	. . . . . 6 ⊢ (t ∈ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC )) ↔ ∃u(u ∈ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∧ ⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC )))
3		vex 2863	. . . . . . . . . . 11 ⊢ u ∈ V
4	3	eluni1 4174	. . . . . . . . . 10 ⊢ (u ∈ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ↔ {u} ∈ ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ))
5		snex 4112	. . . . . . . . . . 11 ⊢ {u} ∈ V
6	5	elcompl 3226	. . . . . . . . . 10 ⊢ ({u} ∈ ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ↔ ¬ {u} ∈ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ))
7		elimapw13 4947	. . . . . . . . . . . 12 ⊢ ({u} ∈ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ↔ ∃m ∈ NC ⟨{{{m}}}, {u}⟩ ∈ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)))
8		spacval 6283	. . . . . . . . . . . . . . . . . 18 ⊢ (m ∈ NC → ( Spac ‘m) = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
9	8	nceqd 6111	. . . . . . . . . . . . . . . . 17 ⊢ (m ∈ NC → Nc ( Spac ‘m) = Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
10	9	eqeq1d 2361	. . . . . . . . . . . . . . . 16 ⊢ (m ∈ NC → ( Nc ( Spac ‘m) = u ↔ Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u))
11		tccl 6161	. . . . . . . . . . . . . . . . . . . 20 ⊢ (m ∈ NC → Tc m ∈ NC )
12		spacval 6283	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( Tc m ∈ NC → ( Spac ‘ Tc m) = Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
13	11, 12	syl 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (m ∈ NC → ( Spac ‘ Tc m) = Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
14	13	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 ⊢ (m ∈ NC → (( Spac ‘ Tc m) ∈ Fin ↔ Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ))
15	13	nceqd 6111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (m ∈ NC → Nc ( Spac ‘ Tc m) = Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
16	15	eqeq1d 2361	. . . . . . . . . . . . . . . . . . 19 ⊢ (m ∈ NC → ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ↔ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c)))
17	15	eqeq1d 2361	. . . . . . . . . . . . . . . . . . 19 ⊢ (m ∈ NC → ( Nc ( Spac ‘ Tc m) = ( Tc u +c 2c) ↔ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))
18	16, 17	orbi12d 690	. . . . . . . . . . . . . . . . . 18 ⊢ (m ∈ NC → (( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c)) ↔ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
19	14, 18	anbi12d 691	. . . . . . . . . . . . . . . . 17 ⊢ (m ∈ NC → ((( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c))) ↔ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
20	19	notbid 285	. . . . . . . . . . . . . . . 16 ⊢ (m ∈ NC → (¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c))) ↔ ¬ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
21	10, 20	anbi12d 691	. . . . . . . . . . . . . . 15 ⊢ (m ∈ NC → (( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c)))) ↔ ( Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u ∧ ¬ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))))
22		eldif 3222	. . . . . . . . . . . . . . . 16 ⊢ (⟨{{{m}}}, {u}⟩ ∈ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ↔ (⟨{{{m}}}, {u}⟩ ∈ SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∧ ¬ ⟨{{{m}}}, {u}⟩ ∈ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)))
23		snex 4112	. . . . . . . . . . . . . . . . . . . 20 ⊢ {{m}} ∈ V
24	23, 3	opsnelsi 5775	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨{{{m}}}, {u}⟩ ∈ SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ↔ ⟨{{m}}, u⟩ ∈ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))
25		opelcnv 4894	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨{{m}}, u⟩ ∈ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ↔ ⟨u, {{m}}⟩ ∈ (◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))
26		opelres 4951	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨u, {{m}}⟩ ∈ (◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ↔ (⟨u, {{m}}⟩ ∈ ◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ∧ u ∈ NC ))
27		opelcnv 4894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨u, {{m}}⟩ ∈ ◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↔ ⟨{{m}}, u⟩ ∈ ( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)))
28		opelco 4885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{{m}}, u⟩ ∈ ( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↔ ∃t({{m}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ t S u))
29		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {m} ∈ V
30	29	brsnsi1 5776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({{m}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ↔ ∃v(t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v))
31	30	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({{m}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ t S u) ↔ (∃v(t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u))
32		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃v((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u) ↔ (∃v(t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u))
33	31, 32	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (({{m}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ t S u) ↔ ∃v((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u))
34	33	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃t({{m}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ t S u) ↔ ∃t∃v((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u))
35		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃t∃v((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u) ↔ ∃v∃t((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u))
36	34, 35	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃t({{m}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ t S u) ↔ ∃v∃t((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u))
37		anass 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u) ↔ (t = {v} ∧ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ t S u)))
38	37	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃t((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u) ↔ ∃t(t = {v} ∧ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ t S u)))
39		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {v} ∈ V
40		breq1 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (t = {v} → (t S u ↔ {v} S u))
41	40	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (t = {v} → (({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ t S u) ↔ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ {v} S u)))
42	39, 41	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃t(t = {v} ∧ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ t S u)) ↔ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ {v} S u))
43		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ↔ v ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c){m})
44		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c){m} ↔ ⟨v, {m}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c))
45		spacvallem1 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))} ∈ V
46	45, 29	nchoicelem10 6299	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨v, {m}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c) ↔ v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
47	43, 44, 46	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ↔ v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
48		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ v ∈ V
49	48, 3	brssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({v} S u ↔ v ∈ u)
50	47, 49	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (({m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v ∧ {v} S u) ↔ (v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ v ∈ u))
51	38, 42, 50	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃t((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u) ↔ (v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ v ∈ u))
52	51	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃v∃t((t = {v} ∧ {m}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)v) ∧ t S u) ↔ ∃v(v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ v ∈ u))
53	28, 36, 52	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨{{m}}, u⟩ ∈ ( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↔ ∃v(v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ v ∈ u))
54	29, 45	clos1ex 5877	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ V
55		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → (v ∈ u ↔ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u))
56	54, 55	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃v(v = Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ v ∈ u) ↔ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u)
57	27, 53, 56	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨u, {{m}}⟩ ∈ ◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↔ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u)
58	57	anbi1i 676	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨u, {{m}}⟩ ∈ ◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ∧ u ∈ NC ) ↔ ( Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u ∧ u ∈ NC ))
59		ancom 437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u ∧ u ∈ NC ) ↔ (u ∈ NC ∧ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u))
60	26, 58, 59	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨u, {{m}}⟩ ∈ (◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ↔ (u ∈ NC ∧ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u))
61	24, 25, 60	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨{{{m}}}, {u}⟩ ∈ SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ↔ (u ∈ NC ∧ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u))
62		eqcom 2355	. . . . . . . . . . . . . . . . . . 19 ⊢ ( Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u ↔ u = Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
63	54	eqnc2 6130	. . . . . . . . . . . . . . . . . . 19 ⊢ (u = Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ↔ (u ∈ NC ∧ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u))
64	62, 63	bitri 240	. . . . . . . . . . . . . . . . . 18 ⊢ ( Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u ↔ (u ∈ NC ∧ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ u))
65	61, 64	bitr4i 243	. . . . . . . . . . . . . . . . 17 ⊢ (⟨{{{m}}}, {u}⟩ ∈ SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ↔ Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u)
66		elimapw11c 4949	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨{{{m}}}, {u}⟩ ∈ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c) ↔ ∃n⟨{{n}}, ⟨{{{m}}}, {u}⟩⟩ ∈ ( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))))
67		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨{{n}}, ⟨{{{m}}}, {u}⟩⟩ ∈ ( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) ↔ (⟨{{n}}, {{{m}}}⟩ ∈ SI SI ◡TcFn ∧ ⟨{{n}}, {u}⟩ ∈ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))))
68		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {n} ∈ V
69	68, 23	opsnelsi 5775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{{n}}, {{{m}}}⟩ ∈ SI SI ◡TcFn ↔ ⟨{n}, {{m}}⟩ ∈ SI ◡TcFn)
70		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ n ∈ V
71	70, 29	opsnelsi 5775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨{n}, {{m}}⟩ ∈ SI ◡TcFn ↔ ⟨n, {m}⟩ ∈ ◡TcFn)
72		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (n◡TcFn{m} ↔ ⟨n, {m}⟩ ∈ ◡TcFn)
73		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (n◡TcFn{m} ↔ {m}TcFnn)
74	71, 72, 73	3bitr2i 264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{n}, {{m}}⟩ ∈ SI ◡TcFn ↔ {m}TcFnn)
75		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ m ∈ V
76	75	brtcfn 6247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({m}TcFnn ↔ n = Tc m)
77	69, 74, 76	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨{{n}}, {{{m}}}⟩ ∈ SI SI ◡TcFn ↔ n = Tc m)
78		opelco 4885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{{n}}, {u}⟩ ∈ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )) ↔ ∃v({{n}}◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )v ∧ v((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ){u}))
79		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({{n}}◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )v ↔ v(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ){{n}})
80		brres 4950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (v(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ){{n}} ↔ (v◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)){{n}} ∧ v ∈ NC ))
81		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (v◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)){{n}} ↔ {{n}} ( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c))v)
82		brco 4884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ({{n}} ( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c))v ↔ ∃u({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ∧ u S v))
83	68	brsnsi1 5776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ↔ ∃t(u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t))
84	83	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ∧ u S v) ↔ (∃t(u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v))
85		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃t((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v) ↔ (∃t(u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v))
86	84, 85	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ∧ u S v) ↔ ∃t((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v))
87	86	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃u({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ∧ u S v) ↔ ∃u∃t((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v))
88		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃u∃t((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v) ↔ ∃t∃u((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v))
89		anass 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v) ↔ (u = {t} ∧ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ u S v)))
90	89	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃u((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v) ↔ ∃u(u = {t} ∧ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ u S v)))
91		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {t} ∈ V
92		breq1 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (u = {t} → (u S v ↔ {t} S v))
93	92	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (u = {t} → (({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ u S v) ↔ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ {t} S v)))
94	91, 93	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃u(u = {t} ∧ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ u S v)) ↔ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ {t} S v))
95		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ↔ t ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c){n})
96		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (t ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c){n} ↔ ⟨t, {n}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c))
97	45, 68	nchoicelem10 6299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨t, {n}⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c) ↔ t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
98	95, 96, 97	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ↔ t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
99		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ t ∈ V
100	99, 48	brssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({t} S v ↔ t ∈ v)
101	98, 100	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (({n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t ∧ {t} S v) ↔ (t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ t ∈ v))
102	90, 94, 101	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∃u((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v) ↔ (t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ t ∈ v))
103	102	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃t∃u((u = {t} ∧ {n}◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)t) ∧ u S v) ↔ ∃t(t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ t ∈ v))
104	87, 88, 103	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃u({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ∧ u S v) ↔ ∃t(t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ t ∈ v))
105		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v ↔ ∃t(t = Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ t ∈ v))
106	104, 105	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃u({{n}} SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)u ∧ u S v) ↔ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v)
107	81, 82, 106	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (v◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)){{n}} ↔ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v)
108	107	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((v◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)){{n}} ∧ v ∈ NC ) ↔ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v ∧ v ∈ NC ))
109		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v ∧ v ∈ NC ) ↔ (v ∈ NC ∧ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v))
110	80, 108, 109	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ){{n}} ↔ (v ∈ NC ∧ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v))
111	68, 45	clos1ex 5877	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ V
112	111	eqnc2 6130	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ↔ (v ∈ NC ∧ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ v))
113	110, 112	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ){{n}} ↔ v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
114	79, 113	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({{n}}◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )v ↔ v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
115		brres 4950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ){u} ↔ (v(◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))){u} ∧ v ∈ Nn ))
116		brco 4884	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (v(◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))){u} ↔ ∃t(v◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))t ∧ t◡TcFn{u}))
117		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (v◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))t ↔ t(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))v)
118		brun 4693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (t(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))v ↔ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {1c})))v ∨ t( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))v))
119		brco 4884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {1c})))v ↔ ∃u(t◡(1st ↾ (◡2nd “ {1c}))u ∧ u AddC v))
120		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (t◡(1st ↾ (◡2nd “ {1c}))u ↔ u(1st ↾ (◡2nd “ {1c}))t)
121		brres 4950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (u(1st ↾ (◡2nd “ {1c}))t ↔ (u1st t ∧ u ∈ (◡2nd “ {1c})))
122		eliniseg 5021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (u ∈ (◡2nd “ {1c}) ↔ u2nd 1c)
123	122	anbi2i 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((u1st t ∧ u ∈ (◡2nd “ {1c})) ↔ (u1st t ∧ u2nd 1c))
124	121, 123	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (u(1st ↾ (◡2nd “ {1c}))t ↔ (u1st t ∧ u2nd 1c))
125		1cex 4143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 1c ∈ V
126	99, 125	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((u1st t ∧ u2nd 1c) ↔ u = ⟨t, 1c⟩)
127	120, 124, 126	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (t◡(1st ↾ (◡2nd “ {1c}))u ↔ u = ⟨t, 1c⟩)
128	127	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((t◡(1st ↾ (◡2nd “ {1c}))u ∧ u AddC v) ↔ (u = ⟨t, 1c⟩ ∧ u AddC v))
129	128	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃u(t◡(1st ↾ (◡2nd “ {1c}))u ∧ u AddC v) ↔ ∃u(u = ⟨t, 1c⟩ ∧ u AddC v))
130	99, 125	opex 4589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ⟨t, 1c⟩ ∈ V
131		breq1 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (u = ⟨t, 1c⟩ → (u AddC v ↔ ⟨t, 1c⟩ AddC v))
132	130, 131	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃u(u = ⟨t, 1c⟩ ∧ u AddC v) ↔ ⟨t, 1c⟩ AddC v)
133	119, 129, 132	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {1c})))v ↔ ⟨t, 1c⟩ AddC v)
134	99, 125	braddcfn 5827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨t, 1c⟩ AddC v ↔ (t +c 1c) = v)
135		eqcom 2355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((t +c 1c) = v ↔ v = (t +c 1c))
136	133, 134, 135	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {1c})))v ↔ v = (t +c 1c))
137		brco 4884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))v ↔ ∃u(t◡(1st ↾ (◡2nd “ {2c}))u ∧ u AddC v))
138		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (t◡(1st ↾ (◡2nd “ {2c}))u ↔ u(1st ↾ (◡2nd “ {2c}))t)
139		brres 4950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (u(1st ↾ (◡2nd “ {2c}))t ↔ (u1st t ∧ u ∈ (◡2nd “ {2c})))
140		eliniseg 5021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (u ∈ (◡2nd “ {2c}) ↔ u2nd 2c)
141	140	anbi2i 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((u1st t ∧ u ∈ (◡2nd “ {2c})) ↔ (u1st t ∧ u2nd 2c))
142	139, 141	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (u(1st ↾ (◡2nd “ {2c}))t ↔ (u1st t ∧ u2nd 2c))
143		2nc 6169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ 2c ∈ NC
144	143	elexi 2869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 2c ∈ V
145	99, 144	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((u1st t ∧ u2nd 2c) ↔ u = ⟨t, 2c⟩)
146	138, 142, 145	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (t◡(1st ↾ (◡2nd “ {2c}))u ↔ u = ⟨t, 2c⟩)
147	146	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((t◡(1st ↾ (◡2nd “ {2c}))u ∧ u AddC v) ↔ (u = ⟨t, 2c⟩ ∧ u AddC v))
148	147	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃u(t◡(1st ↾ (◡2nd “ {2c}))u ∧ u AddC v) ↔ ∃u(u = ⟨t, 2c⟩ ∧ u AddC v))
149	99, 144	opex 4589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ⟨t, 2c⟩ ∈ V
150		breq1 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (u = ⟨t, 2c⟩ → (u AddC v ↔ ⟨t, 2c⟩ AddC v))
151	149, 150	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃u(u = ⟨t, 2c⟩ ∧ u AddC v) ↔ ⟨t, 2c⟩ AddC v)
152	137, 148, 151	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))v ↔ ⟨t, 2c⟩ AddC v)
153	99, 144	braddcfn 5827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨t, 2c⟩ AddC v ↔ (t +c 2c) = v)
154		eqcom 2355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((t +c 2c) = v ↔ v = (t +c 2c))
155	152, 153, 154	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (t( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))v ↔ v = (t +c 2c))
156	136, 155	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((t( AddC ∘ ◡(1st ↾ (◡2nd “ {1c})))v ∨ t( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))v) ↔ (v = (t +c 1c) ∨ v = (t +c 2c)))
157	117, 118, 156	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (v◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))t ↔ (v = (t +c 1c) ∨ v = (t +c 2c)))
158		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (t◡TcFn{u} ↔ {u}TcFnt)
159	3	brtcfn 6247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({u}TcFnt ↔ t = Tc u)
160	158, 159	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t◡TcFn{u} ↔ t = Tc u)
161	157, 160	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))t ∧ t◡TcFn{u}) ↔ ((v = (t +c 1c) ∨ v = (t +c 2c)) ∧ t = Tc u))
162		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((v = (t +c 1c) ∨ v = (t +c 2c)) ∧ t = Tc u) ↔ (t = Tc u ∧ (v = (t +c 1c) ∨ v = (t +c 2c))))
163	161, 162	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((v◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))t ∧ t◡TcFn{u}) ↔ (t = Tc u ∧ (v = (t +c 1c) ∨ v = (t +c 2c))))
164	163	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(v◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))t ∧ t◡TcFn{u}) ↔ ∃t(t = Tc u ∧ (v = (t +c 1c) ∨ v = (t +c 2c))))
165		tcex 6158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Tc u ∈ V
166		addceq1 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t = Tc u → (t +c 1c) = ( Tc u +c 1c))
167	166	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (t = Tc u → (v = (t +c 1c) ↔ v = ( Tc u +c 1c)))
168		addceq1 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t = Tc u → (t +c 2c) = ( Tc u +c 2c))
169	168	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (t = Tc u → (v = (t +c 2c) ↔ v = ( Tc u +c 2c)))
170	167, 169	orbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (t = Tc u → ((v = (t +c 1c) ∨ v = (t +c 2c)) ↔ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c))))
171	165, 170	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(t = Tc u ∧ (v = (t +c 1c) ∨ v = (t +c 2c))) ↔ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)))
172	116, 164, 171	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v(◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))){u} ↔ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)))
173	172	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((v(◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))){u} ∧ v ∈ Nn ) ↔ ((v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)) ∧ v ∈ Nn ))
174		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)) ∧ v ∈ Nn ) ↔ (v ∈ Nn ∧ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c))))
175	115, 173, 174	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (v((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ){u} ↔ (v ∈ Nn ∧ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c))))
176	114, 175	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (({{n}}◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )v ∧ v((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ){u}) ↔ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ (v ∈ Nn ∧ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)))))
177	176	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃v({{n}}◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )v ∧ v((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ){u}) ↔ ∃v(v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ (v ∈ Nn ∧ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)))))
178		ncex 6118	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ V
179		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → (v ∈ Nn ↔ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Nn ))
180		finnc 6244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ↔ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Nn )
181	179, 180	syl6bbr 254	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → (v ∈ Nn ↔ Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ))
182		eqeq1 2359	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → (v = ( Tc u +c 1c) ↔ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c)))
183		eqeq1 2359	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → (v = ( Tc u +c 2c) ↔ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))
184	182, 183	orbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → ((v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)) ↔ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
185	181, 184	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) → ((v ∈ Nn ∧ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c))) ↔ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
186	178, 185	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃v(v = Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∧ (v ∈ Nn ∧ (v = ( Tc u +c 1c) ∨ v = ( Tc u +c 2c)))) ↔ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
187	78, 177, 186	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨{{n}}, {u}⟩ ∈ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )) ↔ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
188	77, 187	anbi12i 678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨{{n}}, {{{m}}}⟩ ∈ SI SI ◡TcFn ∧ ⟨{{n}}, {u}⟩ ∈ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) ↔ (n = Tc m ∧ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
189	67, 188	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨{{n}}, ⟨{{{m}}}, {u}⟩⟩ ∈ ( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) ↔ (n = Tc m ∧ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
190	189	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃n⟨{{n}}, ⟨{{{m}}}, {u}⟩⟩ ∈ ( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) ↔ ∃n(n = Tc m ∧ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
191		tcex 6158	. . . . . . . . . . . . . . . . . . . 20 ⊢ Tc m ∈ V
192		sneq 3745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n = Tc m → {n} = { Tc m})
193		clos1eq1 5875	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({n} = { Tc m} → Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
194	192, 193	syl 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = Tc m → Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
195	194	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (n = Tc m → ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ↔ Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ))
196	194	nceqd 6111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n = Tc m → Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
197	196	eqeq1d 2361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = Tc m → ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ↔ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c)))
198	196	eqeq1d 2361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = Tc m → ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c) ↔ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))
199	197, 198	orbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (n = Tc m → (( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)) ↔ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
200	195, 199	anbi12d 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n = Tc m → (( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))) ↔ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
201	191, 200	ceqsexv 2895	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃n(n = Tc m ∧ ( Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({n}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))) ↔ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
202	66, 190, 201	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨{{{m}}}, {u}⟩ ∈ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c) ↔ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
203	202	notbii 287	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ⟨{{{m}}}, {u}⟩ ∈ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c) ↔ ¬ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c))))
204	65, 203	anbi12i 678	. . . . . . . . . . . . . . . 16 ⊢ ((⟨{{{m}}}, {u}⟩ ∈ SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∧ ¬ ⟨{{{m}}}, {u}⟩ ∈ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ↔ ( Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u ∧ ¬ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
205	22, 204	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (⟨{{{m}}}, {u}⟩ ∈ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ↔ ( Nc Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = u ∧ ¬ ( Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ Fin ∧ ( Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 1c) ∨ Nc Clos1 ({ Tc m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) = ( Tc u +c 2c)))))
206	21, 205	syl6rbbr 255	. . . . . . . . . . . . . 14 ⊢ (m ∈ NC → (⟨{{{m}}}, {u}⟩ ∈ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ↔ ( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c))))))
207		tceq 6159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( Nc ( Spac ‘m) = u → Tc Nc ( Spac ‘m) = Tc u)
208	207	addceq1d 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ ( Nc ( Spac ‘m) = u → ( Tc Nc ( Spac ‘m) +c 1c) = ( Tc u +c 1c))
209	208	eqeq2d 2364	. . . . . . . . . . . . . . . . . 18 ⊢ ( Nc ( Spac ‘m) = u → ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ↔ Nc ( Spac ‘ Tc m) = ( Tc u +c 1c)))
210	207	addceq1d 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ ( Nc ( Spac ‘m) = u → ( Tc Nc ( Spac ‘m) +c 2c) = ( Tc u +c 2c))
211	210	eqeq2d 2364	. . . . . . . . . . . . . . . . . 18 ⊢ ( Nc ( Spac ‘m) = u → ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c) ↔ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c)))
212	209, 211	orbi12d 690	. . . . . . . . . . . . . . . . 17 ⊢ ( Nc ( Spac ‘m) = u → (( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)) ↔ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c))))
213	212	anbi2d 684	. . . . . . . . . . . . . . . 16 ⊢ ( Nc ( Spac ‘m) = u → ((( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))) ↔ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c)))))
214	213	notbid 285	. . . . . . . . . . . . . . 15 ⊢ ( Nc ( Spac ‘m) = u → (¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))) ↔ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c)))))
215	214	pm5.32i 618	. . . . . . . . . . . . . 14 ⊢ (( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ↔ ( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc u +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc u +c 2c)))))
216	206, 215	syl6bbr 254	. . . . . . . . . . . . 13 ⊢ (m ∈ NC → (⟨{{{m}}}, {u}⟩ ∈ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ↔ ( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
217	216	rexbiia 2648	. . . . . . . . . . . 12 ⊢ (∃m ∈ NC ⟨{{{m}}}, {u}⟩ ∈ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ↔ ∃m ∈ NC ( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))
218		rexanali 2661	. . . . . . . . . . . 12 ⊢ (∃m ∈ NC ( Nc ( Spac ‘m) = u ∧ ¬ (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ↔ ¬ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))
219	7, 217, 218	3bitrri 263	. . . . . . . . . . 11 ⊢ (¬ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ↔ {u} ∈ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ))
220	219	con1bii 321	. . . . . . . . . 10 ⊢ (¬ {u} ∈ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ↔ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))
221	4, 6, 220	3bitri 262	. . . . . . . . 9 ⊢ (u ∈ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ↔ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))
222		opelco 4885	. . . . . . . . . . 11 ⊢ (⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) ↔ ∃v(u◡ AddC v ∧ v(2nd ↾ (◡1st “ {1c}))t))
223		brcnv 4893	. . . . . . . . . . . . . 14 ⊢ (u◡ AddC v ↔ v AddC u)
224		brres 4950	. . . . . . . . . . . . . . 15 ⊢ (v(2nd ↾ (◡1st “ {1c}))t ↔ (v2nd t ∧ v ∈ (◡1st “ {1c})))
225		eliniseg 5021	. . . . . . . . . . . . . . . . 17 ⊢ (v ∈ (◡1st “ {1c}) ↔ v1st 1c)
226	225	anbi2i 675	. . . . . . . . . . . . . . . 16 ⊢ ((v2nd t ∧ v ∈ (◡1st “ {1c})) ↔ (v2nd t ∧ v1st 1c))
227		ancom 437	. . . . . . . . . . . . . . . 16 ⊢ ((v2nd t ∧ v1st 1c) ↔ (v1st 1c ∧ v2nd t))
228	226, 227	bitri 240	. . . . . . . . . . . . . . 15 ⊢ ((v2nd t ∧ v ∈ (◡1st “ {1c})) ↔ (v1st 1c ∧ v2nd t))
229	125, 99	op1st2nd 5791	. . . . . . . . . . . . . . 15 ⊢ ((v1st 1c ∧ v2nd t) ↔ v = ⟨1c, t⟩)
230	224, 228, 229	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (v(2nd ↾ (◡1st “ {1c}))t ↔ v = ⟨1c, t⟩)
231	223, 230	anbi12i 678	. . . . . . . . . . . . 13 ⊢ ((u◡ AddC v ∧ v(2nd ↾ (◡1st “ {1c}))t) ↔ (v AddC u ∧ v = ⟨1c, t⟩))
232		ancom 437	. . . . . . . . . . . . 13 ⊢ ((v AddC u ∧ v = ⟨1c, t⟩) ↔ (v = ⟨1c, t⟩ ∧ v AddC u))
233	231, 232	bitri 240	. . . . . . . . . . . 12 ⊢ ((u◡ AddC v ∧ v(2nd ↾ (◡1st “ {1c}))t) ↔ (v = ⟨1c, t⟩ ∧ v AddC u))
234	233	exbii 1582	. . . . . . . . . . 11 ⊢ (∃v(u◡ AddC v ∧ v(2nd ↾ (◡1st “ {1c}))t) ↔ ∃v(v = ⟨1c, t⟩ ∧ v AddC u))
235	125, 99	opex 4589	. . . . . . . . . . . 12 ⊢ ⟨1c, t⟩ ∈ V
236		breq1 4643	. . . . . . . . . . . 12 ⊢ (v = ⟨1c, t⟩ → (v AddC u ↔ ⟨1c, t⟩ AddC u))
237	235, 236	ceqsexv 2895	. . . . . . . . . . 11 ⊢ (∃v(v = ⟨1c, t⟩ ∧ v AddC u) ↔ ⟨1c, t⟩ AddC u)
238	222, 234, 237	3bitri 262	. . . . . . . . . 10 ⊢ (⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) ↔ ⟨1c, t⟩ AddC u)
239	125, 99	braddcfn 5827	. . . . . . . . . 10 ⊢ (⟨1c, t⟩ AddC u ↔ (1c +c t) = u)
240		eqcom 2355	. . . . . . . . . 10 ⊢ ((1c +c t) = u ↔ u = (1c +c t))
241	238, 239, 240	3bitri 262	. . . . . . . . 9 ⊢ (⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) ↔ u = (1c +c t))
242	221, 241	anbi12i 678	. . . . . . . 8 ⊢ ((u ∈ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∧ ⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC )) ↔ (∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ∧ u = (1c +c t)))
243		ancom 437	. . . . . . . 8 ⊢ ((∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ∧ u = (1c +c t)) ↔ (u = (1c +c t) ∧ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
244	242, 243	bitri 240	. . . . . . 7 ⊢ ((u ∈ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∧ ⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC )) ↔ (u = (1c +c t) ∧ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
245	244	exbii 1582	. . . . . 6 ⊢ (∃u(u ∈ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∧ ⟨u, t⟩ ∈ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC )) ↔ ∃u(u = (1c +c t) ∧ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
246	125, 99	addcex 4395	. . . . . . 7 ⊢ (1c +c t) ∈ V
247		eqeq2 2362	. . . . . . . . 9 ⊢ (u = (1c +c t) → ( Nc ( Spac ‘m) = u ↔ Nc ( Spac ‘m) = (1c +c t)))
248	247	imbi1d 308	. . . . . . . 8 ⊢ (u = (1c +c t) → (( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ↔ ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
249	248	ralbidv 2635	. . . . . . 7 ⊢ (u = (1c +c t) → (∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))) ↔ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
250	246, 249	ceqsexv 2895	. . . . . 6 ⊢ (∃u(u = (1c +c t) ∧ ∀m ∈ NC ( Nc ( Spac ‘m) = u → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))) ↔ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))
251	2, 245, 250	3bitri 262	. . . . 5 ⊢ (t ∈ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC )) ↔ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))
252	251	abbi2i 2465	. . . 4 ⊢ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC )) = {t ∣ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))}
253	252	uneq2i 3416	. . 3 ⊢ ({t ∣ ¬ ≤c We NC } ∪ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ))) = ({t ∣ ¬ ≤c We NC } ∪ {t ∣ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))})
254		imor 401	. . . 4 ⊢ (( ≤c We NC → ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))) ↔ (¬ ≤c We NC ∨ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c))))))
255	254	abbii 2466	. . 3 ⊢ {t ∣ ( ≤c We NC → ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))} = {t ∣ (¬ ≤c We NC ∨ ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))}
256	1, 253, 255	3eqtr4i 2383	. 2 ⊢ ({t ∣ ¬ ≤c We NC } ∪ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ))) = {t ∣ ( ≤c We NC → ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))}
257		abexv 4325	. . 3 ⊢ {t ∣ ¬ ≤c We NC } ∈ V
258		2ndex 5113	. . . . . 6 ⊢ 2nd ∈ V
259		1stex 4740	. . . . . . . 8 ⊢ 1st ∈ V
260	259	cnvex 5103	. . . . . . 7 ⊢ ◡1st ∈ V
261		snex 4112	. . . . . . 7 ⊢ {1c} ∈ V
262	260, 261	imaex 4748	. . . . . 6 ⊢ (◡1st “ {1c}) ∈ V
263	258, 262	resex 5118	. . . . 5 ⊢ (2nd ↾ (◡1st “ {1c})) ∈ V
264		addcfnex 5825	. . . . . 6 ⊢ AddC ∈ V
265	264	cnvex 5103	. . . . 5 ⊢ ◡ AddC ∈ V
266	263, 265	coex 4751	. . . 4 ⊢ ((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) ∈ V
267		ssetex 4745	. . . . . . . . . . . . 13 ⊢ S ∈ V
268	267	ins3ex 5799	. . . . . . . . . . . . . . . . . 18 ⊢ Ins3 S ∈ V
269	267	complex 4105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∼ S ∈ V
270	269	cnvex 5103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ◡ ∼ S ∈ V
271	267	cnvex 5103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ◡ S ∈ V
272	45	imageex 5802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))} ∈ V
273	267, 272	coex 4751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ V
274	273	fixex 5790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}) ∈ V
275	271, 274	resex 5118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})) ∈ V
276	270, 275	txpex 5786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))) ∈ V
277	276	rnex 5108	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))) ∈ V
278	277	complex 4105	. . . . . . . . . . . . . . . . . . 19 ⊢ ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))) ∈ V
279	278	ins2ex 5798	. . . . . . . . . . . . . . . . . 18 ⊢ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))) ∈ V
280	268, 279	symdifex 4109	. . . . . . . . . . . . . . . . 17 ⊢ ( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) ∈ V
281	280, 125	imaex 4748	. . . . . . . . . . . . . . . 16 ⊢ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c) ∈ V
282	281	complex 4105	. . . . . . . . . . . . . . 15 ⊢ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c) ∈ V
283	282	cnvex 5103	. . . . . . . . . . . . . 14 ⊢ ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c) ∈ V
284	283	siex 4754	. . . . . . . . . . . . 13 ⊢ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c) ∈ V
285	267, 284	coex 4751	. . . . . . . . . . . 12 ⊢ ( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ∈ V
286	285	cnvex 5103	. . . . . . . . . . 11 ⊢ ◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ∈ V
287		ncsex 6112	. . . . . . . . . . 11 ⊢ NC ∈ V
288	286, 287	resex 5118	. . . . . . . . . 10 ⊢ (◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∈ V
289	288	cnvex 5103	. . . . . . . . 9 ⊢ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∈ V
290	289	siex 4754	. . . . . . . 8 ⊢ SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∈ V
291		tcfnex 6245	. . . . . . . . . . . . 13 ⊢ TcFn ∈ V
292	291	cnvex 5103	. . . . . . . . . . . 12 ⊢ ◡TcFn ∈ V
293	292	siex 4754	. . . . . . . . . . 11 ⊢ SI ◡TcFn ∈ V
294	293	siex 4754	. . . . . . . . . 10 ⊢ SI SI ◡TcFn ∈ V
295	258	cnvex 5103	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡2nd ∈ V
296	295, 261	imaex 4748	. . . . . . . . . . . . . . . . . 18 ⊢ (◡2nd “ {1c}) ∈ V
297	259, 296	resex 5118	. . . . . . . . . . . . . . . . 17 ⊢ (1st ↾ (◡2nd “ {1c})) ∈ V
298	297	cnvex 5103	. . . . . . . . . . . . . . . 16 ⊢ ◡(1st ↾ (◡2nd “ {1c})) ∈ V
299	264, 298	coex 4751	. . . . . . . . . . . . . . 15 ⊢ ( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∈ V
300		snex 4112	. . . . . . . . . . . . . . . . . . 19 ⊢ {2c} ∈ V
301	295, 300	imaex 4748	. . . . . . . . . . . . . . . . . 18 ⊢ (◡2nd “ {2c}) ∈ V
302	259, 301	resex 5118	. . . . . . . . . . . . . . . . 17 ⊢ (1st ↾ (◡2nd “ {2c})) ∈ V
303	302	cnvex 5103	. . . . . . . . . . . . . . . 16 ⊢ ◡(1st ↾ (◡2nd “ {2c})) ∈ V
304	264, 303	coex 4751	. . . . . . . . . . . . . . 15 ⊢ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))) ∈ V
305	299, 304	unex 4107	. . . . . . . . . . . . . 14 ⊢ (( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))) ∈ V
306	305	cnvex 5103	. . . . . . . . . . . . 13 ⊢ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c})))) ∈ V
307	292, 306	coex 4751	. . . . . . . . . . . 12 ⊢ (◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ∈ V
308		nncex 4397	. . . . . . . . . . . 12 ⊢ Nn ∈ V
309	307, 308	resex 5118	. . . . . . . . . . 11 ⊢ ((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∈ V
310	309, 289	coex 4751	. . . . . . . . . 10 ⊢ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC )) ∈ V
311	294, 310	txpex 5786	. . . . . . . . 9 ⊢ ( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) ∈ V
312	125	pw1ex 4304	. . . . . . . . 9 ⊢ ℘11c ∈ V
313	311, 312	imaex 4748	. . . . . . . 8 ⊢ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c) ∈ V
314	290, 313	difex 4108	. . . . . . 7 ⊢ ( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) ∈ V
315	287	pw1ex 4304	. . . . . . . . 9 ⊢ ℘1 NC ∈ V
316	315	pw1ex 4304	. . . . . . . 8 ⊢ ℘1℘1 NC ∈ V
317	316	pw1ex 4304	. . . . . . 7 ⊢ ℘1℘1℘1 NC ∈ V
318	314, 317	imaex 4748	. . . . . 6 ⊢ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∈ V
319	318	complex 4105	. . . . 5 ⊢ ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∈ V
320	319	uni1ex 4294	. . . 4 ⊢ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ) ∈ V
321	266, 320	imaex 4748	. . 3 ⊢ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC )) ∈ V
322	257, 321	unex 4107	. 2 ⊢ ({t ∣ ¬ ≤c We NC } ∪ (((2nd ↾ (◡1st “ {1c})) ∘ ◡ AddC ) “ ⋃1 ∼ (( SI ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ) ∖ (( SI SI ◡TcFn ⊗ (((◡TcFn ∘ ◡(( AddC ∘ ◡(1st ↾ (◡2nd “ {1c}))) ∪ ( AddC ∘ ◡(1st ↾ (◡2nd “ {2c}))))) ↾ Nn ) ∘ ◡(◡( S ∘ SI ◡ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ Image{⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})))) “ 1c)) ↾ NC ))) “ ℘11c)) “ ℘1℘1℘1 NC ))) ∈ V
323	256, 322	eqeltrri 2424	1 ⊢ {t ∣ ( ≤c We NC → ∀m ∈ NC ( Nc ( Spac ‘m) = (1c +c t) → (( Spac ‘ Tc m) ∈ Fin ∧ ( Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) = ( Tc Nc ( Spac ‘m) +c 2c)))))} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2615  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∖ cdif 3207   ∪ cun 3208   ⊕ csymdif 3210  {csn 3738  ⋃₁cuni1 4134  1_cc1c 4135  ℘₁cpw1 4136   Nn cnnc 4374   +_c cplc 4376   Fin cfin 4377  ⟨cop 4562  {copab 4623   class class class wbr 4640  1^st c1st 4718   S csset 4720   SI csi 4721   ∘ ccom 4722   “ cima 4723  ^◡ccnv 4772  ran crn 4774   ↾ cres 4775   ‘cfv 4782  2^nd c2nd 4784  (class class class)co 5526   ⊗ ctxp 5736   Fix cfix 5740   AddC caddcfn 5746   Ins2 cins2 5750   Ins3 cins3 5752  Imagecimage 5754   Clos1 cclos1 5873   We cwe 5896   NC cncs 6089   ≤_c clec 6090   Nc cnc 6092   T_c ctc 6094  2_cc2c 6095   ↑_c cce 6097  TcFnctcfn 6098   Sp_ac cspac 6274

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-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 theorem 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-csb 3138  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-iun 3972  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-cup 5743  df-disj 5745  df-addcfn 5747  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 referenced by:  nchoicelem17  6306