HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem mapenlem1 4469
Description: Lemma for mapen 4471.
Hypotheses
Ref Expression
mapenlem.1 |- A e. V
mapenlem.2 |- B e. V
mapenlem.3 |- C e. V
mapenlem.4 |- D e. V
mapenlem.5 |- H = {<.x, y>. | (x e. (A ^m C) /\ y = ((f o. x) o. `'g))}
Assertion
Ref Expression
mapenlem1 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((H` z)` (g` v)) = (f` (z` v)))
Distinct variable groups:   f,g,x,y,z,v,A   B,f,g,x,y,z,v   C,f,g,x,y,z,v   D,f,g,x,y,z,v   z,H,v
Proof of Theorem mapenlem1
StepHypRef Expression
1 mapenlem.1 . . . . . 6 |- A e. V
2 mapenlem.3 . . . . . 6 |- C e. V
31, 2elmap 4318 . . . . 5 |- (z e. (A ^m C) <-> z:C-->A)
4 coeq2 3271 . . . . . . 7 |- (x = z -> (f o. x) = (f o. z))
54coeq1d 3274 . . . . . 6 |- (x = z -> ((f o. x) o. `'g) = ((f o. z) o. `'g))
6 mapenlem.5 . . . . . 6 |- H = {<.x, y>. | (x e. (A ^m C) /\ y = ((f o. x) o. `'g))}
7 visset 1804 . . . . . . . 8 |- f e. V
8 visset 1804 . . . . . . . 8 |- z e. V
97, 8coex 3511 . . . . . . 7 |- (f o. z) e. V
10 visset 1804 . . . . . . . 8 |- g e. V
1110cnvex 3506 . . . . . . 7 |- `'g e. V
129, 11coex 3511 . . . . . 6 |- ((f o. z) o. `'g) e. V
135, 6, 12fvopab4 3765 . . . . 5 |- (z e. (A ^m C) -> (H` z) = ((f o. z) o. `'g))
143, 13sylbir 201 . . . 4 |- (z:C-->A -> (H` z) = ((f o. z) o. `'g))
1514fveq1d 3711 . . 3 |- (z:C-->A -> ((H` z)` (g` v)) = (((f o. z) o. `'g)` (g` v)))
1615ad2antlr 405 . 2 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((H` z)` (g` v)) = (((f o. z) o. `'g)` (g` v)))
17 f1ococnv1 3694 . . . . . . . . . 10 |- (g:C-1-1-onto->D -> (`'g o. g) = (I |` C))
1817coeq2d 3275 . . . . . . . . 9 |- (g:C-1-1-onto->D -> ((f o. z) o. (`'g o. g)) = ((f o. z) o. (I |` C)))
19 fcoi1 3630 . . . . . . . . 9 |- ((f o. z):C-->B -> ((f o. z) o. (I |` C)) = (f o. z))
2018, 19sylan9eqr 1521 . . . . . . . 8 |- (((f o. z):C-->B /\ g:C-1-1-onto->D) -> ((f o. z) o. (`'g o. g)) = (f o. z))
21 fco 3621 . . . . . . . . 9 |- ((f:A-->B /\ z:C-->A) -> (f o. z):C-->B)
22 f1of 3674 . . . . . . . . 9 |- (f:A-1-1-onto->B -> f:A-->B)
2321, 22sylan 448 . . . . . . . 8 |- ((f:A-1-1-onto->B /\ z:C-->A) -> (f o. z):C-->B)
2420, 23sylan 448 . . . . . . 7 |- (((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) -> ((f o. z) o. (`'g o. g)) = (f o. z))
2524an1rs 488 . . . . . 6 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> ((f o. z) o. (`'g o. g)) = (f o. z))
26 coass 3498 . . . . . 6 |- (((f o. z) o. `'g) o. g) = ((f o. z) o. (`'g o. g))
2725, 26syl5eq 1511 . . . . 5 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> (((f o. z) o. `'g) o. g) = (f o. z))
2827fveq1d 3711 . . . 4 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> ((((f o. z) o. `'g) o. g)` v) = ((f o. z)` v))
2928adantr 389 . . 3 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = ((f o. z)` v))
30 fvco3 3761 . . . . 5 |- ((Fun ((f o. z) o. `'g) /\ g:C-->D /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v)))
31303expa 831 . . . 4 |- (((Fun ((f o. z) o. `'g) /\ g:C-->D) /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v)))
32 funco 3536 . . . . . . . 8 |- ((Fun (f o. z) /\ Fun `'g) -> Fun ((f o. z) o. `'g))
33 funco 3536 . . . . . . . . 9 |- ((Fun f /\ Fun z) -> Fun (f o. z))
34 f1ofun 3676 . . . . . . . . 9 |- (f:A-1-1-onto->B -> Fun f)
35 ffun 3615 . . . . . . . . 9 |- (z:C-->A -> Fun z)
3633, 34, 35syl2an 454 . . . . . . . 8 |- ((f:A-1-1-onto->B /\ z:C-->A) -> Fun (f o. z))
37 f1o3 3679 . . . . . . . . 9 |- (g:C-1-1-onto->D <-> (g:C-onto->D /\ Fun `'g))
3837pm3.27bi 326 . . . . . . . 8 |- (g:C-1-1-onto->D -> Fun `'g)
3932, 36, 38syl2an 454 . . . . . . 7 |- (((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) -> Fun ((f o. z) o. `'g))
40 f1of 3674 . . . . . . 7 |- (g:C-1-1-onto->D -> g:C-->D)
4139, 40anim12i 333 . . . . . 6 |- ((((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) /\ g:C-1-1-onto->D) -> (Fun ((f o. z) o. `'g) /\ g:C-->D))
4241anabss3 499 . . . . 5 |- (((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) -> (Fun ((f o. z) o. `'g) /\ g:C-->D))
4342an1rs 488 . . . 4 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> (Fun ((f o. z) o. `'g) /\ g:C-->D))
4431, 43sylan 448 . . 3 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v)))
45 fvco3 3761 . . . . . . 7 |- ((Fun f /\ z:C-->A /\ v e. C) -> ((f o. z)` v) = (f` (z` v)))
46453expb 832 . . . . . 6 |- ((Fun f /\ (z:C-->A /\ v e. C)) -> ((f o. z)` v) = (f` (z` v)))
4746, 34sylan 448 . . . . 5 |- ((f:A-1-1-onto->B /\ (z:C-->A /\ v e. C)) -> ((f o. z)` v) = (f` (z` v)))
4847adantlr 393 . . . 4 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ (z:C-->A /\ v e. C)) -> ((f o. z)` v) = (f` (z` v)))
4948anassrs 441 . . 3 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((f o. z)` v) = (f` (z` v)))
5029, 44, 493eqtr3d 1507 . 2 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> (((f o. z) o. `'g)` (g` v)) = (f` (z` v)))
5116, 50eqtrd 1499 1 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((H` z)` (g` v)) = (f` (z` v)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955  Vcvv 1802  {copab 2656  Icid 2820  `'ccnv 3159   |` cres 3162   o. ccom 3164  Fun wfun 3166  -->wf 3168  -onto->wfo 3170  -1-1-onto->wf1o 3171  ` cfv 3172  (class class class)co 3948   ^m cm 4306
This theorem is referenced by:  mapenlem2 4470
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-opr 3950  df-oprab 3951  df-map 4308
Copyright terms: Public domain