MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  estrcco Structured version   Visualization version   GIF version

Theorem estrcco 16539
Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.)
Hypotheses
Ref Expression
estrcbas.c 𝐶 = (ExtStrCat‘𝑈)
estrcbas.u (𝜑𝑈𝑉)
estrcco.o · = (comp‘𝐶)
estrcco.x (𝜑𝑋𝑈)
estrcco.y (𝜑𝑌𝑈)
estrcco.z (𝜑𝑍𝑈)
estrcco.a 𝐴 = (Base‘𝑋)
estrcco.b 𝐵 = (Base‘𝑌)
estrcco.d 𝐷 = (Base‘𝑍)
estrcco.f (𝜑𝐹:𝐴𝐵)
estrcco.g (𝜑𝐺:𝐵𝐷)
Assertion
Ref Expression
estrcco (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) = (𝐺𝐹))

Proof of Theorem estrcco
Dummy variables 𝑓 𝑔 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 estrcbas.c . . . 4 𝐶 = (ExtStrCat‘𝑈)
2 estrcbas.u . . . 4 (𝜑𝑈𝑉)
3 estrcco.o . . . 4 · = (comp‘𝐶)
41, 2, 3estrccofval 16538 . . 3 (𝜑· = (𝑣 ∈ (𝑈 × 𝑈), 𝑧𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚 (Base‘(2nd𝑣))), 𝑓 ∈ ((Base‘(2nd𝑣)) ↑𝑚 (Base‘(1st𝑣))) ↦ (𝑔𝑓))))
5 fveq2 6088 . . . . . . 7 (𝑧 = 𝑍 → (Base‘𝑧) = (Base‘𝑍))
65adantl 480 . . . . . 6 ((𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍) → (Base‘𝑧) = (Base‘𝑍))
76adantl 480 . . . . 5 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (Base‘𝑧) = (Base‘𝑍))
8 simprl 789 . . . . . . . 8 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → 𝑣 = ⟨𝑋, 𝑌⟩)
98fveq2d 6092 . . . . . . 7 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (2nd𝑣) = (2nd ‘⟨𝑋, 𝑌⟩))
10 estrcco.x . . . . . . . . 9 (𝜑𝑋𝑈)
11 estrcco.y . . . . . . . . 9 (𝜑𝑌𝑈)
12 op2ndg 7049 . . . . . . . . 9 ((𝑋𝑈𝑌𝑈) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
1310, 11, 12syl2anc 690 . . . . . . . 8 (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
1413adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
159, 14eqtrd 2643 . . . . . 6 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (2nd𝑣) = 𝑌)
1615fveq2d 6092 . . . . 5 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (Base‘(2nd𝑣)) = (Base‘𝑌))
177, 16oveq12d 6545 . . . 4 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → ((Base‘𝑧) ↑𝑚 (Base‘(2nd𝑣))) = ((Base‘𝑍) ↑𝑚 (Base‘𝑌)))
188fveq2d 6092 . . . . . . 7 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (1st𝑣) = (1st ‘⟨𝑋, 𝑌⟩))
1918fveq2d 6092 . . . . . 6 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (Base‘(1st𝑣)) = (Base‘(1st ‘⟨𝑋, 𝑌⟩)))
20 op1stg 7048 . . . . . . . . 9 ((𝑋𝑈𝑌𝑈) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
2110, 11, 20syl2anc 690 . . . . . . . 8 (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
2221fveq2d 6092 . . . . . . 7 (𝜑 → (Base‘(1st ‘⟨𝑋, 𝑌⟩)) = (Base‘𝑋))
2322adantr 479 . . . . . 6 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (Base‘(1st ‘⟨𝑋, 𝑌⟩)) = (Base‘𝑋))
2419, 23eqtrd 2643 . . . . 5 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (Base‘(1st𝑣)) = (Base‘𝑋))
2516, 24oveq12d 6545 . . . 4 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → ((Base‘(2nd𝑣)) ↑𝑚 (Base‘(1st𝑣))) = ((Base‘𝑌) ↑𝑚 (Base‘𝑋)))
26 eqidd 2610 . . . 4 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (𝑔𝑓) = (𝑔𝑓))
2717, 25, 26mpt2eq123dv 6593 . . 3 ((𝜑 ∧ (𝑣 = ⟨𝑋, 𝑌⟩ ∧ 𝑧 = 𝑍)) → (𝑔 ∈ ((Base‘𝑧) ↑𝑚 (Base‘(2nd𝑣))), 𝑓 ∈ ((Base‘(2nd𝑣)) ↑𝑚 (Base‘(1st𝑣))) ↦ (𝑔𝑓)) = (𝑔 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ↦ (𝑔𝑓)))
28 opelxpi 5062 . . . 4 ((𝑋𝑈𝑌𝑈) → ⟨𝑋, 𝑌⟩ ∈ (𝑈 × 𝑈))
2910, 11, 28syl2anc 690 . . 3 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑈 × 𝑈))
30 estrcco.z . . 3 (𝜑𝑍𝑈)
31 ovex 6555 . . . . 5 ((Base‘𝑍) ↑𝑚 (Base‘𝑌)) ∈ V
32 ovex 6555 . . . . 5 ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ∈ V
3331, 32mpt2ex 7113 . . . 4 (𝑔 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ↦ (𝑔𝑓)) ∈ V
3433a1i 11 . . 3 (𝜑 → (𝑔 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ↦ (𝑔𝑓)) ∈ V)
354, 27, 29, 30, 34ovmpt2d 6664 . 2 (𝜑 → (⟨𝑋, 𝑌· 𝑍) = (𝑔 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ↦ (𝑔𝑓)))
36 simpl 471 . . . 4 ((𝑔 = 𝐺𝑓 = 𝐹) → 𝑔 = 𝐺)
37 simpr 475 . . . 4 ((𝑔 = 𝐺𝑓 = 𝐹) → 𝑓 = 𝐹)
3836, 37coeq12d 5196 . . 3 ((𝑔 = 𝐺𝑓 = 𝐹) → (𝑔𝑓) = (𝐺𝐹))
3938adantl 480 . 2 ((𝜑 ∧ (𝑔 = 𝐺𝑓 = 𝐹)) → (𝑔𝑓) = (𝐺𝐹))
40 estrcco.g . . . 4 (𝜑𝐺:𝐵𝐷)
41 estrcco.b . . . . . . 7 𝐵 = (Base‘𝑌)
4241a1i 11 . . . . . 6 (𝜑𝐵 = (Base‘𝑌))
4342eqcomd 2615 . . . . 5 (𝜑 → (Base‘𝑌) = 𝐵)
44 estrcco.d . . . . . . 7 𝐷 = (Base‘𝑍)
4544a1i 11 . . . . . 6 (𝜑𝐷 = (Base‘𝑍))
4645eqcomd 2615 . . . . 5 (𝜑 → (Base‘𝑍) = 𝐷)
4743, 46feq23d 5939 . . . 4 (𝜑 → (𝐺:(Base‘𝑌)⟶(Base‘𝑍) ↔ 𝐺:𝐵𝐷))
4840, 47mpbird 245 . . 3 (𝜑𝐺:(Base‘𝑌)⟶(Base‘𝑍))
49 fvex 6098 . . . . 5 (Base‘𝑍) ∈ V
5049a1i 11 . . . 4 (𝜑 → (Base‘𝑍) ∈ V)
51 fvex 6098 . . . . 5 (Base‘𝑌) ∈ V
5251a1i 11 . . . 4 (𝜑 → (Base‘𝑌) ∈ V)
53 elmapg 7734 . . . 4 (((Base‘𝑍) ∈ V ∧ (Base‘𝑌) ∈ V) → (𝐺 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)) ↔ 𝐺:(Base‘𝑌)⟶(Base‘𝑍)))
5450, 52, 53syl2anc 690 . . 3 (𝜑 → (𝐺 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)) ↔ 𝐺:(Base‘𝑌)⟶(Base‘𝑍)))
5548, 54mpbird 245 . 2 (𝜑𝐺 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)))
56 estrcco.f . . . 4 (𝜑𝐹:𝐴𝐵)
57 estrcco.a . . . . . . 7 𝐴 = (Base‘𝑋)
5857a1i 11 . . . . . 6 (𝜑𝐴 = (Base‘𝑋))
5958eqcomd 2615 . . . . 5 (𝜑 → (Base‘𝑋) = 𝐴)
6059, 43feq23d 5939 . . . 4 (𝜑 → (𝐹:(Base‘𝑋)⟶(Base‘𝑌) ↔ 𝐹:𝐴𝐵))
6156, 60mpbird 245 . . 3 (𝜑𝐹:(Base‘𝑋)⟶(Base‘𝑌))
62 fvex 6098 . . . . 5 (Base‘𝑋) ∈ V
6362a1i 11 . . . 4 (𝜑 → (Base‘𝑋) ∈ V)
64 elmapg 7734 . . . 4 (((Base‘𝑌) ∈ V ∧ (Base‘𝑋) ∈ V) → (𝐹 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ↔ 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
6552, 63, 64syl2anc 690 . . 3 (𝜑 → (𝐹 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)) ↔ 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
6661, 65mpbird 245 . 2 (𝜑𝐹 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋)))
67 coexg 6987 . . 3 ((𝐺 ∈ ((Base‘𝑍) ↑𝑚 (Base‘𝑌)) ∧ 𝐹 ∈ ((Base‘𝑌) ↑𝑚 (Base‘𝑋))) → (𝐺𝐹) ∈ V)
6855, 66, 67syl2anc 690 . 2 (𝜑 → (𝐺𝐹) ∈ V)
6935, 39, 55, 66, 68ovmpt2d 6664 1 (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) = (𝐺𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  Vcvv 3172  cop 4130   × cxp 5026  ccom 5032  wf 5786  cfv 5790  (class class class)co 6527  cmpt2 6529  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  Basecbs 15641  compcco 15726  ExtStrCatcestrc 16531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-fz 12153  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-hom 15739  df-cco 15740  df-estrc 16532
This theorem is referenced by:  estrccatid  16541  funcestrcsetclem9  16557  funcsetcestrclem9  16572  rngcco  41765  rnghmsubcsetclem2  41770  ringcco  41811  rhmsubcsetclem2  41816
  Copyright terms: Public domain W3C validator