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

Theorem nchoicelem16 6304
 Description: Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305. (Contributed by SF, 19-Mar-2015.)
Assertion
Ref Expression
nchoicelem16 {t ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +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.
StepHypRef Expression
1 unab 3521 . . 3 ({t ¬ ≤c We NC } ∪ {t m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))}) = {t (¬ ≤c We NC m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))}
2 elima3 4756 . . . . . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC )) ↔ u(u 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) u, t ((2nd (1st “ {1c})) AddC )))
3 vex 2862 . . . . . . . . . . 11 u V
43eluni1 4173 . . . . . . . . . 10 (u 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) ↔ {u} ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ))
5 snex 4111 . . . . . . . . . . 11 {u} V
65elcompl 3225 . . . . . . . . . 10 ({u} ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) ↔ ¬ {u} (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ))
7 elimapw13 4946 . . . . . . . . . . . 12 ({u} (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) ↔ m NC {{{m}}}, {u} ( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)))
8 spacval 6282 . . . . . . . . . . . . . . . . . 18 (m NC → ( Spacm) = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
98nceqd 6110 . . . . . . . . . . . . . . . . 17 (m NCNc ( Spacm) = Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
109eqeq1d 2361 . . . . . . . . . . . . . . . 16 (m NC → ( Nc ( Spacm) = uNc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = u))
11 tccl 6160 . . . . . . . . . . . . . . . . . . . 20 (m NCTc m NC )
12 spacval 6282 . . . . . . . . . . . . . . . . . . . 20 ( Tc m NC → ( SpacTc m) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
1311, 12syl 15 . . . . . . . . . . . . . . . . . . 19 (m NC → ( SpacTc m) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
1413eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (m NC → (( SpacTc m) Fin Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
1513nceqd 6110 . . . . . . . . . . . . . . . . . . . 20 (m NCNc ( SpacTc m) = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
1615eqeq1d 2361 . . . . . . . . . . . . . . . . . . 19 (m NC → ( Nc ( SpacTc m) = ( Tc u +c 1c) ↔ Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c)))
1715eqeq1d 2361 . . . . . . . . . . . . . . . . . . 19 (m NC → ( Nc ( SpacTc m) = ( Tc u +c 2c) ↔ Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))
1816, 17orbi12d 690 . . . . . . . . . . . . . . . . . 18 (m NC → (( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c)) ↔ ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
1914, 18anbi12d 691 . . . . . . . . . . . . . . . . 17 (m NC → ((( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c))) ↔ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
2019notbid 285 . . . . . . . . . . . . . . . 16 (m NC → (¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c))) ↔ ¬ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
2110, 20anbi12d 691 . . . . . . . . . . . . . . 15 (m NC → (( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c)))) ↔ ( Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = u ¬ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))))
22 eldif 3221 . . . . . . . . . . . . . . . 16 ({{{m}}}, {u} ( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)))
23 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {{m}} V
2423, 3opsnelsi 5774 . . . . . . . . . . . . . . . . . . 19 ({{{m}}}, {u} SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) ↔ {{m}}, u (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ))
25 opelcnv 4893 . . . . . . . . . . . . . . . . . . 19 ({{m}}, u (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) ↔ u, {{m}} (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ))
26 opelres 4950 . . . . . . . . . . . . . . . . . . . 20 (u, {{m}} (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) ↔ (u, {{m}} ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) u NC ))
27 opelcnv 4893 . . . . . . . . . . . . . . . . . . . . . 22 (u, {{m}} ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) ↔ {{m}}, u ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)))
28 opelco 4884 . . . . . . . . . . . . . . . . . . . . . . 23 ({{m}}, u ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) ↔ t({{m}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t t S u))
29 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {m} V
3029brsnsi1 5775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({{m}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)tv(t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v))
3130anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({{m}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc 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 = (2cc 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 = (2cc x))})))) “ 1c)v) t S u))
3331, 32bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({{m}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)v) t S u))
3433exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 (t({{m}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t t S u) ↔ tv((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v) t S u))
35 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . 24 (tv((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v) t S u) ↔ vt((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v) t S u))
3634, 35bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (t({{m}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t t S u) ↔ vt((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc 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 = (2cc x))})))) “ 1c)v t S u)))
3837exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)v t S u)))
39 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {v} V
40 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t = {v} → (t S u ↔ {v} S u))
4140anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t = {v} → (({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v t S u) ↔ ({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v {v} S u)))
4239, 41ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t(t = {v} ({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v t S u)) ↔ ({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v {v} S u))
43 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)vv ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m})
44 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (v ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m} ↔ v, {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c))
45 spacvallem1 6281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {x, y (x NC y NC y = (2cc x))} V
4645, 29nchoicelem10 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (v, {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) ↔ v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
4743, 44, 463bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)vv = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
48 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 v V
4948, 3brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({v} S uv u)
5047, 49anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v {v} S u) ↔ (v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) v u))
5138, 42, 503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 (t((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v) t S u) ↔ (v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) v u))
5251exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (vt((t = {v} {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)v) t S u) ↔ v(v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) v u))
5328, 36, 523bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 ({{m}}, u ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) ↔ v(v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) v u))
5429, 45clos1ex 5876 . . . . . . . . . . . . . . . . . . . . . . 23 Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) V
55 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . 23 (v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) → (v u Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u))
5654, 55ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . 22 (v(v = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) v u) ↔ Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u)
5727, 53, 563bitri 262 . . . . . . . . . . . . . . . . . . . . 21 (u, {{m}} ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) ↔ Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u)
5857anbi1i 676 . . . . . . . . . . . . . . . . . . . 20 ((u, {{m}} ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) u NC ) ↔ ( Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u u NC ))
59 ancom 437 . . . . . . . . . . . . . . . . . . . 20 (( Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u u NC ) ↔ (u NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u))
6026, 58, 593bitri 262 . . . . . . . . . . . . . . . . . . 19 (u, {{m}} (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) ↔ (u NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u))
6124, 25, 603bitri 262 . . . . . . . . . . . . . . . . . 18 ({{{m}}}, {u} SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) ↔ (u NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u))
62 eqcom 2355 . . . . . . . . . . . . . . . . . . 19 ( Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = uu = Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
6354eqnc2 6129 . . . . . . . . . . . . . . . . . . 19 (u = Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) ↔ (u NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u))
6462, 63bitri 240 . . . . . . . . . . . . . . . . . 18 ( Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = u ↔ (u NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) u))
6561, 64bitr4i 243 . . . . . . . . . . . . . . . . 17 ({{{m}}}, {u} SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) ↔ Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = u)
66 elimapw11c 4948 . . . . . . . . . . . . . . . . . . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))))
67 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))))
68 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {n} V
6968, 23opsnelsi 5774 . . . . . . . . . . . . . . . . . . . . . . 23 ({{n}}, {{{m}}} SI SI TcFn ↔ {n}, {{m}} SI TcFn)
70 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . 25 n V
7170, 29opsnelsi 5774 . . . . . . . . . . . . . . . . . . . . . . . 24 ({n}, {{m}} SI TcFn ↔ n, {m} TcFn)
72 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . 24 (nTcFn{m} ↔ n, {m} TcFn)
73 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . 24 (nTcFn{m} ↔ {m}TcFnn)
7471, 72, 733bitr2i 264 . . . . . . . . . . . . . . . . . . . . . . 23 ({n}, {{m}} SI TcFn ↔ {m}TcFnn)
75 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 m V
7675brtcfn 6246 . . . . . . . . . . . . . . . . . . . . . . 23 ({m}TcFnnn = Tc m)
7769, 74, 763bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 ({{n}}, {{{m}}} SI SI TcFn ↔ n = Tc m)
78 opelco 4884 . . . . . . . . . . . . . . . . . . . . . . 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 = (2cc x))})))) “ 1c)) NC )) ↔ v({{n}}(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC )v v((TcFn (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))) Nn ){u}))
79 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({{n}}(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC )vv(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ){{n}})
80 brres 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (v(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ){{n}} ↔ (v( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)){{n}} v NC ))
81 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (v( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)){{n}} ↔ {{n}} ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c))v)
82 brco 4883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({{n}} ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c))vu({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)u u S v))
8368brsnsi1 5775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)ut(u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t))
8483anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc 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 = (2cc 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 = (2cc x))})))) “ 1c)t) u S v))
8684, 85bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)t) u S v))
8786exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (u({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)u u S v) ↔ ut((u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t) u S v))
88 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ut((u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t) u S v) ↔ tu((u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc 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 = (2cc x))})))) “ 1c)t u S v)))
9089exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (u((u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)t u S v)))
91 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {t} V
92 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (u = {t} → (u S v ↔ {t} S v))
9392anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (u = {t} → (({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t u S v) ↔ ({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t {t} S v)))
9491, 93ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (u(u = {t} ({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t u S v)) ↔ ({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t {t} S v))
95 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)tt ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){n})
96 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){n} ↔ t, {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c))
9745, 68nchoicelem10 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t, {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) ↔ t = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}))
9895, 96, 973bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)tt = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}))
99 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 t V
10099, 48brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({t} S vt v)
10198, 100anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (({n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t {t} S v) ↔ (t = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) t v))
10290, 94, 1013bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (u((u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t) u S v) ↔ (t = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) t v))
103102exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (tu((u = {t} {n} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)t) u S v) ↔ t(t = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) t v))
10487, 88, 1033bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (u({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)u u S v) ↔ t(t = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) t v))
105 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) vt(t = Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) t v))
106104, 105bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (u({{n}} SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)u u S v) ↔ Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v)
10781, 82, 1063bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (v( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)){{n}} ↔ Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v)
108107anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((v( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)){{n}} v NC ) ↔ ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v v NC ))
109 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v v NC ) ↔ (v NC Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v))
11080, 108, 1093bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (v(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ){{n}} ↔ (v NC Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v))
11168, 45clos1ex 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) V
112111eqnc2 6129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) ↔ (v NC Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) v))
113110, 112bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (v(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ){{n}} ↔ v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}))
11479, 113bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({{n}}(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC )vv = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}))
115 brres 4949 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (v(TcFn (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))){u} ↔ t(v(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))t tTcFn{u}))
117 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (v(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))tt(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))v)
118 brun 4692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t( AddC (1st (2nd “ {1c})))vu(t(1st (2nd “ {1c}))u u AddC v))
120 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t(1st (2nd “ {1c}))uu(1st (2nd “ {1c}))t)
121 brres 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (u(1st (2nd “ {1c}))t ↔ (u1st t u (2nd “ {1c})))
122 eliniseg 5020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (u (2nd “ {1c}) ↔ u2nd 1c)
123122anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((u1st t u (2nd “ {1c})) ↔ (u1st t u2nd 1c))
124121, 123bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (u(1st (2nd “ {1c}))t ↔ (u1st t u2nd 1c))
125 1cex 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1c V
12699, 125op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((u1st t u2nd 1c) ↔ u = t, 1c)
127120, 124, 1263bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t(1st (2nd “ {1c}))uu = t, 1c)
128127anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((t(1st (2nd “ {1c}))u u AddC v) ↔ (u = t, 1c u AddC v))
129128exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (u(t(1st (2nd “ {1c}))u u AddC v) ↔ u(u = t, 1c u AddC v))
13099, 125opex 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 t, 1c V
131 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (u = t, 1c → (u AddC vt, 1c AddC v))
132130, 131ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (u(u = t, 1c u AddC v) ↔ t, 1c AddC v)
133119, 129, 1323bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t( AddC (1st (2nd “ {1c})))vt, 1c AddC v)
13499, 125braddcfn 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t, 1c AddC v ↔ (t +c 1c) = v)
135 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((t +c 1c) = vv = (t +c 1c))
136133, 134, 1353bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t( AddC (1st (2nd “ {1c})))vv = (t +c 1c))
137 brco 4883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t( AddC (1st (2nd “ {2c})))vu(t(1st (2nd “ {2c}))u u AddC v))
138 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t(1st (2nd “ {2c}))uu(1st (2nd “ {2c}))t)
139 brres 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (u(1st (2nd “ {2c}))t ↔ (u1st t u (2nd “ {2c})))
140 eliniseg 5020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (u (2nd “ {2c}) ↔ u2nd 2c)
141140anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((u1st t u (2nd “ {2c})) ↔ (u1st t u2nd 2c))
142139, 141bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (u(1st (2nd “ {2c}))t ↔ (u1st t u2nd 2c))
143 2nc 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2c NC
144143elexi 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2c V
14599, 144op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((u1st t u2nd 2c) ↔ u = t, 2c)
146138, 142, 1453bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t(1st (2nd “ {2c}))uu = t, 2c)
147146anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((t(1st (2nd “ {2c}))u u AddC v) ↔ (u = t, 2c u AddC v))
148147exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (u(t(1st (2nd “ {2c}))u u AddC v) ↔ u(u = t, 2c u AddC v))
14999, 144opex 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 t, 2c V
150 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (u = t, 2c → (u AddC vt, 2c AddC v))
151149, 150ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (u(u = t, 2c u AddC v) ↔ t, 2c AddC v)
152137, 148, 1513bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t( AddC (1st (2nd “ {2c})))vt, 2c AddC v)
15399, 144braddcfn 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t, 2c AddC v ↔ (t +c 2c) = v)
154 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((t +c 2c) = vv = (t +c 2c))
155152, 153, 1543bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t( AddC (1st (2nd “ {2c})))vv = (t +c 2c))
156136, 155orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((t( AddC (1st (2nd “ {1c})))v t( AddC (1st (2nd “ {2c})))v) ↔ (v = (t +c 1c) v = (t +c 2c)))
157117, 118, 1563bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (v(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))t ↔ (v = (t +c 1c) v = (t +c 2c)))
158 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (tTcFn{u} ↔ {u}TcFnt)
1593brtcfn 6246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({u}TcFntt = Tc u)
160158, 159bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (tTcFn{u} ↔ t = Tc u)
161157, 160anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((v(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))t tTcFn{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))))
163161, 162bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((v(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))t tTcFn{u}) ↔ (t = Tc u (v = (t +c 1c) v = (t +c 2c))))
164163exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(v(( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))t tTcFn{u}) ↔ t(t = Tc u (v = (t +c 1c) v = (t +c 2c))))
165 tcex 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Tc u V
166 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = Tc u → (t +c 1c) = ( Tc u +c 1c))
167166eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = Tc u → (v = (t +c 1c) ↔ v = ( Tc u +c 1c)))
168 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = Tc u → (t +c 2c) = ( Tc u +c 2c))
169168eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = Tc u → (v = (t +c 2c) ↔ v = ( Tc u +c 2c)))
170167, 169orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t = Tc u → ((v = (t +c 1c) v = (t +c 2c)) ↔ (v = ( Tc u +c 1c) v = ( Tc u +c 2c))))
171165, 170ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t = Tc u (v = (t +c 1c) v = (t +c 2c))) ↔ (v = ( Tc u +c 1c) v = ( Tc u +c 2c)))
172116, 164, 1713bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (v(TcFn (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))){u} ↔ (v = ( Tc u +c 1c) v = ( Tc u +c 2c)))
173172anbi1i 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))))
175115, 173, 1743bitri 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))))
176114, 175anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 (({{n}}(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))}) (v Nn (v = ( Tc u +c 1c) v = ( Tc u +c 2c)))))
177176exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (v({{n}}(( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))}) (v Nn (v = ( Tc u +c 1c) v = ( Tc u +c 2c)))))
178 ncex 6117 . . . . . . . . . . . . . . . . . . . . . . . 24 Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) V
179 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) → (v NnNc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Nn ))
180 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) FinNc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Nn )
181179, 180syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . . . . 25 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) → (v Nn Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ))
182 eqeq1 2359 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) → (v = ( Tc u +c 1c) ↔ Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c)))
183 eqeq1 2359 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) → (v = ( Tc u +c 2c) ↔ Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))
184182, 183orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) → ((v = ( Tc u +c 1c) v = ( Tc u +c 2c)) ↔ ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
185181, 184anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) → ((v Nn (v = ( Tc u +c 1c) v = ( Tc u +c 2c))) ↔ ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
186178, 185ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (v(v = Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) (v Nn (v = ( Tc u +c 1c) v = ( Tc u +c 2c)))) ↔ ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
18778, 177, 1863bitri 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 = (2cc x))})))) “ 1c)) NC )) ↔ ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
18877, 187anbi12i 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 = (2cc x))})))) “ 1c)) NC ))) ↔ (n = Tc m ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
18967, 188bitri 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 = (2cc x))})))) “ 1c)) NC ))) ↔ (n = Tc m ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
190189exbii 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 = (2cc x))})))) “ 1c)) NC ))) ↔ n(n = Tc m ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
191 tcex 6157 . . . . . . . . . . . . . . . . . . . 20 Tc m V
192 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . 23 (n = Tc m → {n} = { Tc m})
193 clos1eq1 5874 . . . . . . . . . . . . . . . . . . . . . . 23 ({n} = { Tc m} → Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
194192, 193syl 15 . . . . . . . . . . . . . . . . . . . . . 22 (n = Tc m Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
195194eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (n = Tc m → ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
196194nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . 23 (n = Tc mNc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
197196eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . 22 (n = Tc m → ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) ↔ Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c)))
198196eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . 22 (n = Tc m → ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c) ↔ Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))
199197, 198orbi12d 690 . . . . . . . . . . . . . . . . . . . . 21 (n = Tc m → (( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)) ↔ ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
200195, 199anbi12d 691 . . . . . . . . . . . . . . . . . . . 20 (n = Tc m → (( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))) ↔ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
201191, 200ceqsexv 2894 . . . . . . . . . . . . . . . . . . 19 (n(n = Tc m ( Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({n}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))) ↔ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
20266, 190, 2013bitri 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c) ↔ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
203202notbii 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c) ↔ ¬ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c))))
20465, 203anbi12i 678 . . . . . . . . . . . . . . . 16 (({{{m}}}, {u} SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) ↔ ( Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = u ¬ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
20522, 204bitri 240 . . . . . . . . . . . . . . 15 ({{{m}}}, {u} ( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) ↔ ( Nc Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) = u ¬ ( Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) Fin ( Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 1c) Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) = ( Tc u +c 2c)))))
20621, 205syl6rbbr 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) ↔ ( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c))))))
207 tceq 6158 . . . . . . . . . . . . . . . . . . . 20 ( Nc ( Spacm) = uTc Nc ( Spacm) = Tc u)
208207addceq1d 4389 . . . . . . . . . . . . . . . . . . 19 ( Nc ( Spacm) = u → ( Tc Nc ( Spacm) +c 1c) = ( Tc u +c 1c))
209208eqeq2d 2364 . . . . . . . . . . . . . . . . . 18 ( Nc ( Spacm) = u → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) ↔ Nc ( SpacTc m) = ( Tc u +c 1c)))
210207addceq1d 4389 . . . . . . . . . . . . . . . . . . 19 ( Nc ( Spacm) = u → ( Tc Nc ( Spacm) +c 2c) = ( Tc u +c 2c))
211210eqeq2d 2364 . . . . . . . . . . . . . . . . . 18 ( Nc ( Spacm) = u → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c) ↔ Nc ( SpacTc m) = ( Tc u +c 2c)))
212209, 211orbi12d 690 . . . . . . . . . . . . . . . . 17 ( Nc ( Spacm) = u → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c))))
213212anbi2d 684 . . . . . . . . . . . . . . . 16 ( Nc ( Spacm) = u → ((( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))) ↔ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c)))))
214213notbid 285 . . . . . . . . . . . . . . 15 ( Nc ( Spacm) = u → (¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))) ↔ ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c)))))
215214pm5.32i 618 . . . . . . . . . . . . . 14 (( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc u +c 1c) Nc ( SpacTc m) = ( Tc u +c 2c)))))
216206, 215syl6bbr 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) ↔ ( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
217216rexbiia 2647 . . . . . . . . . . . 12 (m NC {{{m}}}, {u} ( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) ↔ m NC ( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
218 rexanali 2660 . . . . . . . . . . . 12 (m NC ( Nc ( Spacm) = u ¬ (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ¬ m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
2197, 217, 2183bitrri 263 . . . . . . . . . . 11 m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ {u} (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ))
220219con1bii 321 . . . . . . . . . 10 (¬ {u} (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) ↔ m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
2214, 6, 2203bitri 262 . . . . . . . . 9 (u 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) ↔ m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
222 opelco 4884 . . . . . . . . . . 11 (u, t ((2nd (1st “ {1c})) AddC ) ↔ v(u AddC v v(2nd (1st “ {1c}))t))
223 brcnv 4892 . . . . . . . . . . . . . 14 (u AddC vv AddC u)
224 brres 4949 . . . . . . . . . . . . . . 15 (v(2nd (1st “ {1c}))t ↔ (v2nd t v (1st “ {1c})))
225 eliniseg 5020 . . . . . . . . . . . . . . . . 17 (v (1st “ {1c}) ↔ v1st 1c)
226225anbi2i 675 . . . . . . . . . . . . . . . 16 ((v2nd t v (1st “ {1c})) ↔ (v2nd t v1st 1c))
227 ancom 437 . . . . . . . . . . . . . . . 16 ((v2nd t v1st 1c) ↔ (v1st 1c v2nd t))
228226, 227bitri 240 . . . . . . . . . . . . . . 15 ((v2nd t v (1st “ {1c})) ↔ (v1st 1c v2nd t))
229125, 99op1st2nd 5790 . . . . . . . . . . . . . . 15 ((v1st 1c v2nd t) ↔ v = 1c, t)
230224, 228, 2293bitri 262 . . . . . . . . . . . . . 14 (v(2nd (1st “ {1c}))tv = 1c, t)
231223, 230anbi12i 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))
233231, 232bitri 240 . . . . . . . . . . . 12 ((u AddC v v(2nd (1st “ {1c}))t) ↔ (v = 1c, t v AddC u))
234233exbii 1582 . . . . . . . . . . 11 (v(u AddC v v(2nd (1st “ {1c}))t) ↔ v(v = 1c, t v AddC u))
235125, 99opex 4588 . . . . . . . . . . . 12 1c, t V
236 breq1 4642 . . . . . . . . . . . 12 (v = 1c, t → (v AddC u1c, t AddC u))
237235, 236ceqsexv 2894 . . . . . . . . . . 11 (v(v = 1c, t v AddC u) ↔ 1c, t AddC u)
238222, 234, 2373bitri 262 . . . . . . . . . 10 (u, t ((2nd (1st “ {1c})) AddC ) ↔ 1c, t AddC u)
239125, 99braddcfn 5826 . . . . . . . . . 10 (1c, t AddC u ↔ (1c +c t) = u)
240 eqcom 2355 . . . . . . . . . 10 ((1c +c t) = uu = (1c +c t))
241238, 239, 2403bitri 262 . . . . . . . . 9 (u, t ((2nd (1st “ {1c})) AddC ) ↔ u = (1c +c t))
242221, 241anbi12i 678 . . . . . . . 8 ((u 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) u, t ((2nd (1st “ {1c})) AddC )) ↔ (m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) u = (1c +c t)))
243 ancom 437 . . . . . . . 8 ((m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) u = (1c +c t)) ↔ (u = (1c +c t) m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
244242, 243bitri 240 . . . . . . 7 ((u 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) u, t ((2nd (1st “ {1c})) AddC )) ↔ (u = (1c +c t) m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
245244exbii 1582 . . . . . 6 (u(u 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) u, t ((2nd (1st “ {1c})) AddC )) ↔ u(u = (1c +c t) m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
246125, 99addcex 4394 . . . . . . 7 (1c +c t) V
247 eqeq2 2362 . . . . . . . . 9 (u = (1c +c t) → ( Nc ( Spacm) = uNc ( Spacm) = (1c +c t)))
248247imbi1d 308 . . . . . . . 8 (u = (1c +c t) → (( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
249248ralbidv 2634 . . . . . . 7 (u = (1c +c t) → (m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
250246, 249ceqsexv 2894 . . . . . 6 (u(u = (1c +c t) m NC ( Nc ( Spacm) = u → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ↔ m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
2512, 245, 2503bitri 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC )) ↔ m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
252251abbi2i 2464 . . . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC )) = {t m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))}
253252uneq2i 3415 . . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ))) = ({t ¬ ≤c We NC } ∪ {t m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))})
254 imor 401 . . . 4 (( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ↔ (¬ ≤c We NC m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
255254abbii 2465 . . 3 {t ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))} = {t (¬ ≤c We NC m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))}
2561, 253, 2553eqtr4i 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ))) = {t ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))}
257 abexv 4324 . . 3 {t ¬ ≤c We NC } V
258 2ndex 5112 . . . . . 6 2nd V
259 1stex 4739 . . . . . . . 8 1st V
260259cnvex 5102 . . . . . . 7 1st V
261 snex 4111 . . . . . . 7 {1c} V
262260, 261imaex 4747 . . . . . 6 (1st “ {1c}) V
263258, 262resex 5117 . . . . 5 (2nd (1st “ {1c})) V
265264cnvex 5102 . . . . 5 AddC V
266263, 265coex 4750 . . . 4 ((2nd (1st “ {1c})) AddC ) V
267 ssetex 4744 . . . . . . . . . . . . 13 S V
268267ins3ex 5798 . . . . . . . . . . . . . . . . . 18 Ins3 S V
269267complex 4104 . . . . . . . . . . . . . . . . . . . . . . 23 S V
270269cnvex 5102 . . . . . . . . . . . . . . . . . . . . . 22 S V
271267cnvex 5102 . . . . . . . . . . . . . . . . . . . . . . 23 S V
27245imageex 5801 . . . . . . . . . . . . . . . . . . . . . . . . 25 Image{x, y (x NC y NC y = (2cc x))} V
273267, 272coex 4750 . . . . . . . . . . . . . . . . . . . . . . . 24 ( S Image{x, y (x NC y NC y = (2cc x))}) V
274273fixex 5789 . . . . . . . . . . . . . . . . . . . . . . 23 Fix ( S Image{x, y (x NC y NC y = (2cc x))}) V
275271, 274resex 5117 . . . . . . . . . . . . . . . . . . . . . 22 ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})) V
276270, 275txpex 5785 . . . . . . . . . . . . . . . . . . . . 21 ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
277276rnex 5107 . . . . . . . . . . . . . . . . . . . 20 ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
278277complex 4104 . . . . . . . . . . . . . . . . . . 19 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
279278ins2ex 5797 . . . . . . . . . . . . . . . . . 18 Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
280268, 279symdifex 4108 . . . . . . . . . . . . . . . . 17 ( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) V
281280, 125imaex 4747 . . . . . . . . . . . . . . . 16 (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
282281complex 4104 . . . . . . . . . . . . . . 15 ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
283282cnvex 5102 . . . . . . . . . . . . . 14 ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
284283siex 4753 . . . . . . . . . . . . 13 SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
285267, 284coex 4750 . . . . . . . . . . . 12 ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) V
286285cnvex 5102 . . . . . . . . . . 11 ( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) V
287 ncsex 6111 . . . . . . . . . . 11 NC V
288286, 287resex 5117 . . . . . . . . . 10 (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) V
289288cnvex 5102 . . . . . . . . 9 (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) V
290289siex 4753 . . . . . . . 8 SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c)) NC ) V
291 tcfnex 6244 . . . . . . . . . . . . 13 TcFn V
292291cnvex 5102 . . . . . . . . . . . 12 TcFn V
293292siex 4753 . . . . . . . . . . 11 SI TcFn V
294293siex 4753 . . . . . . . . . 10 SI SI TcFn V
295258cnvex 5102 . . . . . . . . . . . . . . . . . . 19 2nd V
296295, 261imaex 4747 . . . . . . . . . . . . . . . . . 18 (2nd “ {1c}) V
297259, 296resex 5117 . . . . . . . . . . . . . . . . 17 (1st (2nd “ {1c})) V
298297cnvex 5102 . . . . . . . . . . . . . . . 16 (1st (2nd “ {1c})) V
299264, 298coex 4750 . . . . . . . . . . . . . . 15 ( AddC (1st (2nd “ {1c}))) V
300 snex 4111 . . . . . . . . . . . . . . . . . . 19 {2c} V
301295, 300imaex 4747 . . . . . . . . . . . . . . . . . 18 (2nd “ {2c}) V
302259, 301resex 5117 . . . . . . . . . . . . . . . . 17 (1st (2nd “ {2c})) V
303302cnvex 5102 . . . . . . . . . . . . . . . 16 (1st (2nd “ {2c})) V
304264, 303coex 4750 . . . . . . . . . . . . . . 15 ( AddC (1st (2nd “ {2c}))) V
305299, 304unex 4106 . . . . . . . . . . . . . 14 (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c})))) V
306305cnvex 5102 . . . . . . . . . . . . 13 (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c})))) V
307292, 306coex 4750 . . . . . . . . . . . 12 (TcFn (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))) V
308 nncex 4396 . . . . . . . . . . . 12 Nn V
309307, 308resex 5117 . . . . . . . . . . 11 ((TcFn (( AddC (1st (2nd “ {1c}))) ∪ ( AddC (1st (2nd “ {2c}))))) Nn ) V
310309, 289coex 4750 . . . . . . . . . 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 = (2cc x))})))) “ 1c)) NC )) V
311294, 310txpex 5785 . . . . . . . . 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 = (2cc x))})))) “ 1c)) NC ))) V
312125pw1ex 4303 . . . . . . . . 9 11c V
313311, 312imaex 4747 . . . . . . . 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c) V
314290, 313difex 4107 . . . . . . 7 ( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) V
315287pw1ex 4303 . . . . . . . . 9 1 NC V
316315pw1ex 4303 . . . . . . . 8 11 NC V
317316pw1ex 4303 . . . . . . 7 111 NC V
318314, 317imaex 4747 . . . . . 6 (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) V
319318complex 4104 . . . . 5 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) V
320319uni1ex 4293 . . . 4 1 ∼ (( SI (( S SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ) V
321266, 320imaex 4747 . . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC )) V
322257, 321unex 4106 . 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 = (2cc 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 = (2cc x))})))) “ 1c)) NC ))) “ 11c)) “ 111 NC ))) V
323256, 322eqeltrri 2424 1 {t ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))} V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ⊕ csymdif 3209  {csn 3737  ⋃1cuni1 4133  1cc1c 4134  ℘1cpw1 4135   Nn cnnc 4373   +c cplc 4375   Fin cfin 4376  ⟨cop 4561  {copab 4622   class class class wbr 4639  1st c1st 4717   S csset 4719   SI csi 4720   ∘ ccom 4721   “ cima 4722  ◡ccnv 4771  ran crn 4773   ↾ cres 4774   ‘cfv 4781  2nd c2nd 4783  (class class class)co 5525   ⊗ ctxp 5735   Fix cfix 5739   AddC caddcfn 5745   Ins2 cins2 5749   Ins3 cins3 5751  Imagecimage 5753   Clos1 cclos1 5872   We cwe 5895   NC cncs 6088   ≤c clec 6089   Nc cnc 6091   Tc ctc 6093  2cc2c 6094   ↑c cce 6096  TcFnctcfn 6097   Spac cspac 6273 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-csb 3137  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-fix 5740  df-cup 5742  df-disj 5744  df-addcfn 5746  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-pw1fn 5766  df-fullfun 5768  df-clos1 5873  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-map 6001  df-en 6029  df-ncs 6098  df-nc 6101  df-tc 6103  df-2c 6104  df-ce 6106  df-tcfn 6107  df-spac 6274 This theorem is referenced by:  nchoicelem17  6305
 Copyright terms: Public domain W3C validator