Table of ContentsTable of Contents Mathbox for Frédéric Liné < Previous   Next >
Related theorems
Unicode version
Theorem mapmapmap 14486
Description: Function returning a composite.
Hypothesis
Ref Expression
injsurinj.1 |- F1 = (f e. (B ^m A) |-> ((E o. f) o. G))
Assertion
Ref Expression
mapmapmap |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1:(B ^m A)-->(B1 ^m A1))
Distinct variable groups:   A,f   f,A1   B,f   f,B1   f,E   f,G
Proof of Theorem mapmapmap
StepHypRef Expression
1 ffnfv 4801 . 2 |- (F1:(B ^m A)-->(B1 ^m A1) <-> (F1 Fn (B ^m A) /\ A.x e. (B ^m A)(F1` x) e. (B1 ^m A1)))
2 coexg 4429 . . . . . . . 8 |- ((E e. _V /\ f e. _V) -> (E o. f) e. _V)
3 fex 4595 . . . . . . . . . . . 12 |- ((E:B-->B1 /\ B e. _V) -> E e. _V)
43expcom 403 . . . . . . . . . . 11 |- (B e. _V -> (E:B-->B1 -> E e. _V))
54ad2antlr 441 . . . . . . . . . 10 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> (E:B-->B1 -> E e. _V))
65impcom 378 . . . . . . . . 9 |- ((E:B-->B1 /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> E e. _V)
763adant2 895 . . . . . . . 8 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> E e. _V)
8 visset 2295 . . . . . . . 8 |- f e. _V
92, 7, 8sylancl 525 . . . . . . 7 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (E o. f) e. _V)
10 fex 4595 . . . . . . . . . . . 12 |- ((G:A1-->A /\ A1 e. _V) -> G e. _V)
1110expcom 403 . . . . . . . . . . 11 |- (A1 e. _V -> (G:A1-->A -> G e. _V))
1211ad2antrl 442 . . . . . . . . . 10 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> (G:A1-->A -> G e. _V))
1312com12 14 . . . . . . . . 9 |- (G:A1-->A -> (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> G e. _V))
1413a1i 8 . . . . . . . 8 |- (E:B-->B1 -> (G:A1-->A -> (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> G e. _V)))
15143imp 1061 . . . . . . 7 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> G e. _V)
169, 15jca 310 . . . . . 6 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> ((E o. f) e. _V /\ G e. _V))
1716adantr 425 . . . . 5 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ f e. (B ^m A)) -> ((E o. f) e. _V /\ G e. _V))
1817r19.21aiva 2176 . . . 4 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> A.f e. (B ^m A)((E o. f) e. _V /\ G e. _V))
19 coexg 4429 . . . . 5 |- (((E o. f) e. _V /\ G e. _V) -> ((E o. f) o. G) e. _V)
2019ralimi 2168 . . . 4 |- (A.f e. (B ^m A)((E o. f) e. _V /\ G e. _V) -> A.f e. (B ^m A)((E o. f) o. G) e. _V)
2118, 20syl 12 . . 3 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> A.f e. (B ^m A)((E o. f) o. G) e. _V)
22 injsurinj.1 . . . 4 |- F1 = (f e. (B ^m A) |-> ((E o. f) o. G))
2322fopab2ga 14478 . . 3 |- (A.f e. (B ^m A)((E o. f) o. G) e. _V <-> F1 Fn (B ^m A))
2421, 23sylib 215 . 2 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1 Fn (B ^m A))
25 simpr 350 . . . . . . 7 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> x e. (B ^m A))
26 coexg 4429 . . . . . . . . 9 |- ((E e. _V /\ x e. _V) -> (E o. x) e. _V)
277adantr 425 . . . . . . . . 9 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> E e. _V)
28 visset 2295 . . . . . . . . 9 |- x e. _V
2926, 27, 28sylancl 525 . . . . . . . 8 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (E o. x) e. _V)
3015adantr 425 . . . . . . . 8 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> G e. _V)
31 coexg 4429 . . . . . . . 8 |- (((E o. x) e. _V /\ G e. _V) -> ((E o. x) o. G) e. _V)
3229, 30, 31syl11anc 524 . . . . . . 7 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> ((E o. x) o. G) e. _V)
3325, 32jca 310 . . . . . 6 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (x e. (B ^m A) /\ ((E o. x) o. G) e. _V))
34 coeq2 4124 . . . . . . . 8 |- (f = x -> (E o. f) = (E o. x))
3534coeq1d 4127 . . . . . . 7 |- (f = x -> ((E o. f) o. G) = ((E o. x) o. G))
3635, 22fvmptg 5014 . . . . . 6 |- ((x e. (B ^m A) /\ ((E o. x) o. G) e. _V) -> (F1` x) = ((E o. x) o. G))
37 simpl1 879 . . . . . . . . . . 11 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> E:B-->B1)
38 pm3.22 486 . . . . . . . . . . . . . . 15 |- ((A e. _V /\ B e. _V) -> (B e. _V /\ A e. _V))
3938adantr 425 . . . . . . . . . . . . . 14 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> (B e. _V /\ A e. _V))
40393ad2ant3 899 . . . . . . . . . . . . 13 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (B e. _V /\ A e. _V))
41 elmapg 5392 . . . . . . . . . . . . 13 |- ((B e. _V /\ A e. _V) -> (x e. (B ^m A) <-> x:A-->B))
4240, 41syl 12 . . . . . . . . . . . 12 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (x e. (B ^m A) <-> x:A-->B))
4342biimpa 460 . . . . . . . . . . 11 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> x:A-->B)
44 fco 4573 . . . . . . . . . . 11 |- ((E:B-->B1 /\ x:A-->B) -> (E o. x):A-->B1)
4537, 43, 44syl11anc 524 . . . . . . . . . 10 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (E o. x):A-->B1)
46 simpl2 880 . . . . . . . . . 10 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> G:A1-->A)
4745, 46jca 310 . . . . . . . . 9 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> ((E o. x):A-->B1 /\ G:A1-->A))
4847a1i 8 . . . . . . . 8 |- ((F1` x) = ((E o. x) o. G) -> (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> ((E o. x):A-->B1 /\ G:A1-->A)))
49 fco 4573 . . . . . . . 8 |- (((E o. x):A-->B1 /\ G:A1-->A) -> ((E o. x) o. G):A1-->B1)
5048, 49syl6 25 . . . . . . 7 |- ((F1` x) = ((E o. x) o. G) -> (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> ((E o. x) o. G):A1-->B1))
51 feq1 4551 . . . . . . 7 |- ((F1` x) = ((E o. x) o. G) -> ((F1` x):A1-->B1 <-> ((E o. x) o. G):A1-->B1))
5250, 51sylibrd 221 . . . . . 6 |- ((F1` x) = ((E o. x) o. G) -> (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (F1` x):A1-->B1))
5333, 36, 523syl 24 . . . . 5 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (F1` x):A1-->B1))
5453pm2.43i 78 . . . 4 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (F1` x):A1-->B1)
55 pm3.22 486 . . . . . . . 8 |- ((A1 e. _V /\ B1 e. _V) -> (B1 e. _V /\ A1 e. _V))
5655adantl 424 . . . . . . 7 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> (B1 e. _V /\ A1 e. _V))
57563ad2ant3 899 . . . . . 6 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (B1 e. _V /\ A1 e. _V))
5857adantr 425 . . . . 5 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (B1 e. _V /\ A1 e. _V))
59 elmapg 5392 . . . . 5 |- ((B1 e. _V /\ A1 e. _V) -> ((F1` x) e. (B1 ^m A1) <-> (F1` x):A1-->B1))
6058, 59syl 12 . . . 4 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> ((F1` x) e. (B1 ^m A1) <-> (F1` x):A1-->B1))
6154, 60mpbird 213 . . 3 |- (((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) /\ x e. (B ^m A)) -> (F1` x) e. (B1 ^m A1))
6261r19.21aiva 2176 . 2 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> A.x e. (B ^m A)(F1` x) e. (B1 ^m A1))
631, 24, 62sylanbrc 527 1 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1:(B ^m A)-->(B1 ^m A1))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   o. ccom 3990   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884   e. cmpt 5004   ^m cmap 5381
This theorem is referenced by:  injsurinj 14487
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-map 5383
Copyright terms: Public domain