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

Theorem nchoicelem11 6299
 Description: Lemma for nchoice 6308. Set up stratification for nchoicelem12 6300. (Contributed by SF, 18-Mar-2015.)
Assertion
Ref Expression
nchoicelem11 {t m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn )} V
Distinct variable group:   t,m

Proof of Theorem nchoicelem11
Dummy variables a b u x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . 5 t V
21elcompl 3225 . . . 4 (t ∼ ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) ↔ ¬ t ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ))
3 elimapw13 4946 . . . . . . 7 (t ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) ↔ m NC {{{m}}}, t (((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)))
4 tccl 6160 . . . . . . . . . . . . . 14 (m NCTc m NC )
5 spacval 6282 . . . . . . . . . . . . . 14 ( Tc m NC → ( SpacTc m) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
64, 5syl 15 . . . . . . . . . . . . 13 (m NC → ( SpacTc m) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
76nceqd 6110 . . . . . . . . . . . 12 (m NCNc ( SpacTc m) = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
87eqeq2d 2364 . . . . . . . . . . 11 (m NC → (t = Nc ( SpacTc m) ↔ t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))})))
9 finnc 6243 . . . . . . . . . . . 12 (( Spacm) FinNc ( Spacm) Nn )
10 spacval 6282 . . . . . . . . . . . . 13 (m NC → ( Spacm) = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
1110eleq1d 2419 . . . . . . . . . . . 12 (m NC → (( Spacm) Fin Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
129, 11syl5bbr 250 . . . . . . . . . . 11 (m NC → ( Nc ( Spacm) Nn Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
138, 12imbi12d 311 . . . . . . . . . 10 (m NC → ((t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ (t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) → Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin )))
1413notbid 285 . . . . . . . . 9 (m NC → (¬ (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ ¬ (t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) → Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin )))
15 eldif 3221 . . . . . . . . . 10 ({{{m}}}, t (((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) ↔ ({{{m}}}, t ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) ¬ {{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)))
16 opelco 4884 . . . . . . . . . . . . . 14 ({{{m}}}, t ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) ↔ a({{{m}}} SI SI TcFna a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
17 snex 4111 . . . . . . . . . . . . . . . . . . 19 {{m}} V
1817brsnsi1 5775 . . . . . . . . . . . . . . . . . 18 ({{{m}}} SI SI TcFnab(a = {b} {{m}} SI TcFnb))
1918anbi1i 676 . . . . . . . . . . . . . . . . 17 (({{{m}}} SI SI TcFna a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (b(a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
20 19.41v 1901 . . . . . . . . . . . . . . . . . 18 (b((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (b(a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
2120bicomi 193 . . . . . . . . . . . . . . . . 17 ((b(a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ b((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
2219, 21bitri 240 . . . . . . . . . . . . . . . 16 (({{{m}}} SI SI TcFna a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ b((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
2322exbii 1582 . . . . . . . . . . . . . . 15 (a({{{m}}} SI SI TcFna a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ab((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
24 excom 1741 . . . . . . . . . . . . . . . 16 (ab((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ba((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
25 anass 630 . . . . . . . . . . . . . . . . . . . 20 (((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (a = {b} ({{m}} SI TcFnb a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)))
2625exbii 1582 . . . . . . . . . . . . . . . . . . 19 (a((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ a(a = {b} ({{m}} SI TcFnb a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)))
27 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {b} V
28 breq1 4642 . . . . . . . . . . . . . . . . . . . . 21 (a = {b} → (a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t ↔ {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
2928anbi2d 684 . . . . . . . . . . . . . . . . . . . 20 (a = {b} → (({{m}} SI TcFnb a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)))
3027, 29ceqsexv 2894 . . . . . . . . . . . . . . . . . . 19 (a(a = {b} ({{m}} SI TcFnb a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)) ↔ ({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
3126, 30bitri 240 . . . . . . . . . . . . . . . . . 18 (a((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
3231exbii 1582 . . . . . . . . . . . . . . . . 17 (ba((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ b({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
33 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22 {m} V
3433brsnsi1 5775 . . . . . . . . . . . . . . . . . . . . 21 ({{m}} SI TcFnbu(b = {u} {m}TcFnu))
3534anbi1i 676 . . . . . . . . . . . . . . . . . . . 20 (({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (u(b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
36 19.41v 1901 . . . . . . . . . . . . . . . . . . . 20 (u((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (u(b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
3735, 36bitr4i 243 . . . . . . . . . . . . . . . . . . 19 (({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
3837exbii 1582 . . . . . . . . . . . . . . . . . 18 (b({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ bu((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
39 excom 1741 . . . . . . . . . . . . . . . . . . 19 (bu((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ub((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
40 anass 630 . . . . . . . . . . . . . . . . . . . . . 22 (((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (b = {u} ({m}TcFnu {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)))
4140exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 (b((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ b(b = {u} ({m}TcFnu {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)))
42 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22 {u} V
43 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . . 24 (b = {u} → {b} = {{u}})
4443breq1d 4649 . . . . . . . . . . . . . . . . . . . . . . 23 (b = {u} → ({b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t ↔ {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
4544anbi2d 684 . . . . . . . . . . . . . . . . . . . . . 22 (b = {u} → (({m}TcFnu {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)))
4642, 45ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . 21 (b(b = {u} ({m}TcFnu {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t)) ↔ ({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
4741, 46bitri 240 . . . . . . . . . . . . . . . . . . . 20 (b((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ ({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
4847exbii 1582 . . . . . . . . . . . . . . . . . . 19 (ub((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
4939, 48bitri 240 . . . . . . . . . . . . . . . . . 18 (bu((b = {u} {m}TcFnu) {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
5038, 49bitri 240 . . . . . . . . . . . . . . . . 17 (b({{m}} SI TcFnb {b}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
5132, 50bitri 240 . . . . . . . . . . . . . . . 16 (ba((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
5224, 51bitri 240 . . . . . . . . . . . . . . 15 (ab((a = {b} {{m}} SI TcFnb) a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
5323, 52bitri 240 . . . . . . . . . . . . . 14 (a({{{m}}} SI SI TcFna a(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
5416, 53bitri 240 . . . . . . . . . . . . 13 ({{{m}}}, t ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) ↔ u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t))
55 vex 2862 . . . . . . . . . . . . . . . 16 m V
5655brtcfn 6246 . . . . . . . . . . . . . . 15 ({m}TcFnuu = Tc m)
57 df-br 4640 . . . . . . . . . . . . . . . . 17 ({{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t{{u}}, t (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )))
58 opelcnv 4893 . . . . . . . . . . . . . . . . . 18 ({{u}}, t (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) ↔ t, {{u}} (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )))
59 elin 3219 . . . . . . . . . . . . . . . . . . 19 (t, {{u}} (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) ↔ (t, {{u}} ( NC × V) t, {{u}} ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )))
60 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {{u}} V
61 opelxp 4811 . . . . . . . . . . . . . . . . . . . . 21 (t, {{u}} ( NC × V) ↔ (t NC {{u}} V))
6260, 61mpbiran2 885 . . . . . . . . . . . . . . . . . . . 20 (t, {{u}} ( NC × V) ↔ t NC )
63 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}) ↔ (b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}} t S b))
6442brsnsi2 5776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}} ↔ a(b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}))
6564anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}} t S b) ↔ (a(b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
6663, 65bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}) ↔ (a(b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
67 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ (a(b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
6866, 67bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}) ↔ a((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
6968exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (b(t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}) ↔ ba((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
70 excom 1741 . . . . . . . . . . . . . . . . . . . . . . 23 (ba((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ ab((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
7169, 70bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (b(t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}) ↔ ab((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b))
72 anass 630 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ (b = {a} (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S b)))
7372exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ b(b = {a} (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S b)))
74 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {a} V
75 breq2 4643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b = {a} → (t S bt S {a}))
7675anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b = {a} → ((a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S b) ↔ (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S {a})))
7774, 76ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b(b = {a} (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S b)) ↔ (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S {a}))
7873, 77bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (b((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S {a}))
79 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} ↔ a, {u} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c))
80 spacvallem1 6281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {x, y (x NC y NC y = (2cc x))} V
8180, 42nchoicelem10 6298 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a, {u} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) ↔ a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}))
8279, 81bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} ↔ a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}))
83 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t S {a} ↔ {a} S t)
84 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 a V
8584, 1brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({a} S ta t)
8683, 85bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t S {a} ↔ a t)
8782, 86anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u} t S {a}) ↔ (a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) a t))
8878, 87bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (b((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ (a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) a t))
8988exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (ab((b = {a} a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){u}) t S b) ↔ a(a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) a t))
9071, 89bitri 240 . . . . . . . . . . . . . . . . . . . . 21 (b(t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}) ↔ a(a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) a t))
91 opelco 4884 . . . . . . . . . . . . . . . . . . . . 21 (t, {{u}} ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ) ↔ b(t S b b SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){{u}}))
92 df-clel 2349 . . . . . . . . . . . . . . . . . . . . 21 ( Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) ta(a = Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) a t))
9390, 91, 923bitr4i 268 . . . . . . . . . . . . . . . . . . . 20 (t, {{u}} ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ) ↔ Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) t)
9462, 93anbi12i 678 . . . . . . . . . . . . . . . . . . 19 ((t, {{u}} ( NC × V) t, {{u}} ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) ↔ (t NC Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) t))
9559, 94bitri 240 . . . . . . . . . . . . . . . . . 18 (t, {{u}} (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) ↔ (t NC Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) t))
9658, 95bitri 240 . . . . . . . . . . . . . . . . 17 ({{u}}, t (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) ↔ (t NC Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) t))
9757, 96bitri 240 . . . . . . . . . . . . . . . 16 ({{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t ↔ (t NC Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) t))
9842, 80clos1ex 5876 . . . . . . . . . . . . . . . . 17 Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) V
9998eqnc2 6129 . . . . . . . . . . . . . . . 16 (t = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) ↔ (t NC Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) t))
10097, 99bitr4i 243 . . . . . . . . . . . . . . 15 ({{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))tt = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}))
10156, 100anbi12i 678 . . . . . . . . . . . . . 14 (({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ (u = Tc m t = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))})))
102101exbii 1582 . . . . . . . . . . . . 13 (u({m}TcFnu {{u}}(( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ))t) ↔ u(u = Tc m t = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))})))
10354, 102bitri 240 . . . . . . . . . . . 12 ({{{m}}}, t ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) ↔ u(u = Tc m t = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))})))
104 tcex 6157 . . . . . . . . . . . . 13 Tc m V
105 sneq 3744 . . . . . . . . . . . . . . . 16 (u = Tc m → {u} = { Tc m})
106 clos1eq1 5874 . . . . . . . . . . . . . . . 16 ({u} = { Tc m} → Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
107105, 106syl 15 . . . . . . . . . . . . . . 15 (u = Tc m Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) = Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
108107nceqd 6110 . . . . . . . . . . . . . 14 (u = Tc mNc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
109108eqeq2d 2364 . . . . . . . . . . . . 13 (u = Tc m → (t = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))}) ↔ t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))})))
110104, 109ceqsexv 2894 . . . . . . . . . . . 12 (u(u = Tc m t = Nc Clos1 ({u}, {x, y (x NC y NC y = (2cc x))})) ↔ t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
111103, 110bitri 240 . . . . . . . . . . 11 ({{{m}}}, t ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) ↔ t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}))
112 df-br 4640 . . . . . . . . . . . . . . 15 (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m} ↔ a, {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c))
11380, 33nchoicelem10 6298 . . . . . . . . . . . . . . 15 (a, {m} ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) ↔ a = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
114112, 113bitri 240 . . . . . . . . . . . . . 14 (a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m} ↔ a = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
115114rexbii 2639 . . . . . . . . . . . . 13 (a Fin a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m} ↔ a Fin a = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
116 opelxp 4811 . . . . . . . . . . . . . . 15 ({{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V) ↔ ({{{m}}} 11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) t V))
1171, 116mpbiran2 885 . . . . . . . . . . . . . 14 ({{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V) ↔ {{{m}}} 11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ))
118 snelpw1 4146 . . . . . . . . . . . . . . 15 ({{{m}}} 11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) ↔ {{m}} 1( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ))
119 snelpw1 4146 . . . . . . . . . . . . . . . 16 ({{m}} 1( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) ↔ {m} ( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ))
120 elima 4754 . . . . . . . . . . . . . . . 16 ({m} ( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) ↔ a Fin a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m})
121119, 120bitri 240 . . . . . . . . . . . . . . 15 ({{m}} 1( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) ↔ a Fin a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m})
122118, 121bitri 240 . . . . . . . . . . . . . 14 ({{{m}}} 11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) ↔ a Fin a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m})
123117, 122bitri 240 . . . . . . . . . . . . 13 ({{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V) ↔ a Fin a ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c){m})
124 risset 2661 . . . . . . . . . . . . 13 ( Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fina Fin a = Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
125115, 123, 1243bitr4i 268 . . . . . . . . . . . 12 ({{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V) ↔ Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin )
126125notbii 287 . . . . . . . . . . 11 {{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V) ↔ ¬ Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin )
127111, 126anbi12i 678 . . . . . . . . . 10 (({{{m}}}, t ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) ¬ {{{m}}}, t (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) ↔ (t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) ¬ Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
128 annim 414 . . . . . . . . . 10 ((t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) ¬ Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin ) ↔ ¬ (t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) → Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
12915, 127, 1283bitri 262 . . . . . . . . 9 ({{{m}}}, t (((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) ↔ ¬ (t = Nc Clos1 ({ Tc m}, {x, y (x NC y NC y = (2cc x))}) → Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}) Fin ))
13014, 129syl6rbbr 255 . . . . . . . 8 (m NC → ({{{m}}}, t (((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) ↔ ¬ (t = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
131130rexbiia 2647 . . . . . . 7 (m NC {{{m}}}, t (((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) ↔ m NC ¬ (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
1323, 131bitri 240 . . . . . 6 (t ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) ↔ m NC ¬ (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
133 rexnal 2625 . . . . . 6 (m NC ¬ (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ ¬ m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
134132, 133bitr2i 241 . . . . 5 m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ t ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ))
135134con1bii 321 . . . 4 t ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) ↔ m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
1362, 135bitri 240 . . 3 (t ∼ ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) ↔ m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
137136abbi2i 2464 . 2 ∼ ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) = {t m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn )}
138 ncsex 6111 . . . . . . . . 9 NC V
139 vvex 4109 . . . . . . . . 9 V V
140138, 139xpex 5115 . . . . . . . 8 ( NC × V) V
141 ssetex 4744 . . . . . . . . . . . . . 14 S V
142141ins3ex 5798 . . . . . . . . . . . . 13 Ins3 S V
143141complex 4104 . . . . . . . . . . . . . . . . . 18 S V
144143cnvex 5102 . . . . . . . . . . . . . . . . 17 S V
145141cnvex 5102 . . . . . . . . . . . . . . . . . 18 S V
14680imageex 5801 . . . . . . . . . . . . . . . . . . . 20 Image{x, y (x NC y NC y = (2cc x))} V
147141, 146coex 4750 . . . . . . . . . . . . . . . . . . 19 ( S Image{x, y (x NC y NC y = (2cc x))}) V
148147fixex 5789 . . . . . . . . . . . . . . . . . 18 Fix ( S Image{x, y (x NC y NC y = (2cc x))}) V
149145, 148resex 5117 . . . . . . . . . . . . . . . . 17 ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})) V
150144, 149txpex 5785 . . . . . . . . . . . . . . . 16 ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
151150rnex 5107 . . . . . . . . . . . . . . 15 ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
152151complex 4104 . . . . . . . . . . . . . 14 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
153152ins2ex 5797 . . . . . . . . . . . . 13 Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))}))) V
154142, 153symdifex 4108 . . . . . . . . . . . 12 ( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) V
155 1cex 4142 . . . . . . . . . . . 12 1c V
156154, 155imaex 4747 . . . . . . . . . . 11 (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
157156complex 4104 . . . . . . . . . 10 ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
158157siex 4753 . . . . . . . . 9 SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) V
159158, 145coex 4750 . . . . . . . 8 ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S ) V
160140, 159inex 4105 . . . . . . 7 (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) V
161160cnvex 5102 . . . . . 6 (( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) V
162 tcfnex 6244 . . . . . . . 8 TcFn V
163162siex 4753 . . . . . . 7 SI TcFn V
164163siex 4753 . . . . . 6 SI SI TcFn V
165161, 164coex 4750 . . . . 5 ((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) V
166 finex 4397 . . . . . . . . 9 Fin V
167157, 166imaex 4747 . . . . . . . 8 ( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) V
168167pw1ex 4303 . . . . . . 7 1( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) V
169168pw1ex 4303 . . . . . 6 11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) V
170169, 139xpex 5115 . . . . 5 (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V) V
171165, 170difex 4107 . . . 4 (((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) V
172138pw1ex 4303 . . . . . 6 1 NC V
173172pw1ex 4303 . . . . 5 11 NC V
174173pw1ex 4303 . . . 4 111 NC V
175171, 174imaex 4747 . . 3 ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) V
176175complex 4104 . 2 ∼ ((((( NC × V) ∩ ( SI ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) S )) SI SI TcFn) (11( ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S Image{x, y (x NC y NC y = (2cc x))})))) “ 1c) “ Fin ) × V)) “ 111 NC ) V
177137, 176eqeltrri 2424 1 {t m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn )} V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∩ cin 3208   ⊕ csymdif 3209  {csn 3737  1cc1c 4134  ℘1cpw1 4135   Nn cnnc 4373   Fin cfin 4376  ⟨cop 4561  {copab 4622   class class class wbr 4639   S csset 4719   SI csi 4720   ∘ ccom 4721   “ cima 4722   × cxp 4770  ◡ccnv 4771  ran crn 4773   ↾ cres 4774   ‘cfv 4781  (class class class)co 5525   ⊗ ctxp 5735   Fix cfix 5739   Ins2 cins2 5749   Ins3 cins3 5751  Imagecimage 5753   Clos1 cclos1 5872   NC cncs 6088   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-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-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-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:  nchoicelem12  6300
 Copyright terms: Public domain W3C validator