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

Theorem moni 17070
 Description: Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
ismon.b 𝐵 = (Base‘𝐶)
ismon.h 𝐻 = (Hom ‘𝐶)
ismon.o · = (comp‘𝐶)
ismon.s 𝑀 = (Mono‘𝐶)
ismon.c (𝜑𝐶 ∈ Cat)
ismon.x (𝜑𝑋𝐵)
ismon.y (𝜑𝑌𝐵)
moni.z (𝜑𝑍𝐵)
moni.f (𝜑𝐹 ∈ (𝑋𝑀𝑌))
moni.g (𝜑𝐺 ∈ (𝑍𝐻𝑋))
moni.k (𝜑𝐾 ∈ (𝑍𝐻𝑋))
Assertion
Ref Expression
moni (𝜑 → ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) ↔ 𝐺 = 𝐾))

Proof of Theorem moni
Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 moni.f . . . . 5 (𝜑𝐹 ∈ (𝑋𝑀𝑌))
2 ismon.b . . . . . 6 𝐵 = (Base‘𝐶)
3 ismon.h . . . . . 6 𝐻 = (Hom ‘𝐶)
4 ismon.o . . . . . 6 · = (comp‘𝐶)
5 ismon.s . . . . . 6 𝑀 = (Mono‘𝐶)
6 ismon.c . . . . . 6 (𝜑𝐶 ∈ Cat)
7 ismon.x . . . . . 6 (𝜑𝑋𝐵)
8 ismon.y . . . . . 6 (𝜑𝑌𝐵)
92, 3, 4, 5, 6, 7, 8ismon2 17068 . . . . 5 (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧𝐵𝑔 ∈ (𝑧𝐻𝑋)∀ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = ))))
101, 9mpbid 235 . . . 4 (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧𝐵𝑔 ∈ (𝑧𝐻𝑋)∀ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = )))
1110simprd 499 . . 3 (𝜑 → ∀𝑧𝐵𝑔 ∈ (𝑧𝐻𝑋)∀ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = ))
12 moni.z . . . 4 (𝜑𝑍𝐵)
13 moni.g . . . . . . 7 (𝜑𝐺 ∈ (𝑍𝐻𝑋))
1413adantr 484 . . . . . 6 ((𝜑𝑧 = 𝑍) → 𝐺 ∈ (𝑍𝐻𝑋))
15 simpr 488 . . . . . . 7 ((𝜑𝑧 = 𝑍) → 𝑧 = 𝑍)
1615oveq1d 7170 . . . . . 6 ((𝜑𝑧 = 𝑍) → (𝑧𝐻𝑋) = (𝑍𝐻𝑋))
1714, 16eleqtrrd 2855 . . . . 5 ((𝜑𝑧 = 𝑍) → 𝐺 ∈ (𝑧𝐻𝑋))
18 moni.k . . . . . . . . 9 (𝜑𝐾 ∈ (𝑍𝐻𝑋))
1918adantr 484 . . . . . . . 8 ((𝜑𝑧 = 𝑍) → 𝐾 ∈ (𝑍𝐻𝑋))
2019, 16eleqtrrd 2855 . . . . . . 7 ((𝜑𝑧 = 𝑍) → 𝐾 ∈ (𝑧𝐻𝑋))
2120adantr 484 . . . . . 6 (((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) → 𝐾 ∈ (𝑧𝐻𝑋))
22 simpllr 775 . . . . . . . . . . 11 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → 𝑧 = 𝑍)
2322opeq1d 4772 . . . . . . . . . 10 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → ⟨𝑧, 𝑋⟩ = ⟨𝑍, 𝑋⟩)
2423oveq1d 7170 . . . . . . . . 9 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → (⟨𝑧, 𝑋· 𝑌) = (⟨𝑍, 𝑋· 𝑌))
25 eqidd 2759 . . . . . . . . 9 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → 𝐹 = 𝐹)
26 simplr 768 . . . . . . . . 9 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → 𝑔 = 𝐺)
2724, 25, 26oveq123d 7176 . . . . . . . 8 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → (𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐺))
28 simpr 488 . . . . . . . . 9 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → = 𝐾)
2924, 25, 28oveq123d 7176 . . . . . . . 8 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → (𝐹(⟨𝑧, 𝑋· 𝑌)) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾))
3027, 29eqeq12d 2774 . . . . . . 7 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → ((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) ↔ (𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾)))
3126, 28eqeq12d 2774 . . . . . . 7 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → (𝑔 = 𝐺 = 𝐾))
3230, 31imbi12d 348 . . . . . 6 ((((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) ∧ = 𝐾) → (((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = ) ↔ ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) → 𝐺 = 𝐾)))
3321, 32rspcdv 3535 . . . . 5 (((𝜑𝑧 = 𝑍) ∧ 𝑔 = 𝐺) → (∀ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = ) → ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) → 𝐺 = 𝐾)))
3417, 33rspcimdv 3533 . . . 4 ((𝜑𝑧 = 𝑍) → (∀𝑔 ∈ (𝑧𝐻𝑋)∀ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = ) → ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) → 𝐺 = 𝐾)))
3512, 34rspcimdv 3533 . . 3 (𝜑 → (∀𝑧𝐵𝑔 ∈ (𝑧𝐻𝑋)∀ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋· 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋· 𝑌)) → 𝑔 = ) → ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) → 𝐺 = 𝐾)))
3611, 35mpd 15 . 2 (𝜑 → ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) → 𝐺 = 𝐾))
37 oveq2 7163 . 2 (𝐺 = 𝐾 → (𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾))
3836, 37impbid1 228 1 (𝜑 → ((𝐹(⟨𝑍, 𝑋· 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋· 𝑌)𝐾) ↔ 𝐺 = 𝐾))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ⟨cop 4531  ‘cfv 6339  (class class class)co 7155  Basecbs 16546  Hom chom 16639  compcco 16640  Catccat 16998  Monocmon 17062 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7158  df-oprab 7159  df-mpo 7160  df-1st 7698  df-2nd 7699  df-cat 17002  df-mon 17064 This theorem is referenced by:  epii  17077  monsect  17117  fthmon  17261  setcmon  17418
 Copyright terms: Public domain W3C validator