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

Theorem termoeu1 17126
Description: Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 18-Apr-2020.)
Hypotheses
Ref Expression
termoeu1.c (𝜑𝐶 ∈ Cat)
termoeu1.a (𝜑𝐴 ∈ (TermO‘𝐶))
termoeu1.b (𝜑𝐵 ∈ (TermO‘𝐶))
Assertion
Ref Expression
termoeu1 (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝐶,𝑓   𝜑,𝑓

Proof of Theorem termoeu1
Dummy variables 𝑎 𝑔 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 termoeu1.b . . 3 (𝜑𝐵 ∈ (TermO‘𝐶))
2 eqid 2772 . . . 4 (Base‘𝐶) = (Base‘𝐶)
3 eqid 2772 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
4 termoeu1.c . . . 4 (𝜑𝐶 ∈ Cat)
52, 3, 4istermoi 17112 . . 3 ((𝜑𝐵 ∈ (TermO‘𝐶)) → (𝐵 ∈ (Base‘𝐶) ∧ ∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵)))
61, 5mpdan 674 . 2 (𝜑 → (𝐵 ∈ (Base‘𝐶) ∧ ∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵)))
7 termoeu1.a . . . . 5 (𝜑𝐴 ∈ (TermO‘𝐶))
82, 3, 4istermoi 17112 . . . . 5 ((𝜑𝐴 ∈ (TermO‘𝐶)) → (𝐴 ∈ (Base‘𝐶) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)))
97, 8mpdan 674 . . . 4 (𝜑 → (𝐴 ∈ (Base‘𝐶) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)))
10 oveq1 6977 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎(Hom ‘𝐶)𝐵) = (𝐴(Hom ‘𝐶)𝐵))
1110eleq2d 2845 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) ↔ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)))
1211eubidv 2599 . . . . . . . 8 (𝑎 = 𝐴 → (∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) ↔ ∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)))
1312rspcv 3525 . . . . . . 7 (𝐴 ∈ (Base‘𝐶) → (∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) → ∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)))
14 eqid 2772 . . . . . . . . . . . . . 14 (Iso‘𝐶) = (Iso‘𝐶)
154adantr 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
16 simprl 758 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → 𝐴 ∈ (Base‘𝐶))
17 simprr 760 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → 𝐵 ∈ (Base‘𝐶))
182, 3, 14, 15, 16, 17isohom 16894 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → (𝐴(Iso‘𝐶)𝐵) ⊆ (𝐴(Hom ‘𝐶)𝐵))
1918adantr 473 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴))) → (𝐴(Iso‘𝐶)𝐵) ⊆ (𝐴(Hom ‘𝐶)𝐵))
20 euex 2590 . . . . . . . . . . . . . . 15 (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → ∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵))
2120a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → ∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)))
22 oveq1 6977 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝐵 → (𝑏(Hom ‘𝐶)𝐴) = (𝐵(Hom ‘𝐶)𝐴))
2322eleq2d 2845 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝐵 → (𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) ↔ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)))
2423eubidv 2599 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐵 → (∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) ↔ ∃!𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)))
2524rspcva 3527 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ (Base‘𝐶) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → ∃!𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴))
26 euex 2590 . . . . . . . . . . . . . . . . 17 (∃!𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴) → ∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴))
2725, 26syl 17 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ (Base‘𝐶) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → ∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴))
2827ex 405 . . . . . . . . . . . . . . 15 (𝐵 ∈ (Base‘𝐶) → (∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) → ∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)))
2928ad2antll 716 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → (∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) → ∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)))
30 eqid 2772 . . . . . . . . . . . . . . . . . . . . 21 (Inv‘𝐶) = (Inv‘𝐶)
3115ad2antrr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) ∧ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐶 ∈ Cat)
3216ad2antrr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) ∧ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐴 ∈ (Base‘𝐶))
3317ad2antrr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) ∧ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐵 ∈ (Base‘𝐶))
344, 7, 12termoinv 17125 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝑓(𝐴(Inv‘𝐶)𝐵)𝑔)
3534ad4ant134 1154 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) ∧ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝑓(𝐴(Inv‘𝐶)𝐵)𝑔)
362, 30, 31, 32, 33, 14, 35inviso1 16884 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) ∧ 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
3736ex 405 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) → (𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))
3837eximdv 1876 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) → (∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))
3938expcom 406 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴) → ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → (∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))
4039exlimiv 1889 . . . . . . . . . . . . . . . 16 (∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴) → ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → (∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))
4140com3l 89 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → (∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → (∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))
4241impd 402 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → ((∃𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∃𝑔 𝑔 ∈ (𝐵(Hom ‘𝐶)𝐴)) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))
4321, 29, 42syl2and 598 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) → ((∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))
4443imp 398 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴))) → ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
45 simprl 758 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴))) → ∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵))
46 euelss 4172 . . . . . . . . . . . 12 (((𝐴(Iso‘𝐶)𝐵) ⊆ (𝐴(Hom ‘𝐶)𝐵) ∧ ∃𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵) ∧ ∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵)) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
4719, 44, 45, 46syl3anc 1351 . . . . . . . . . . 11 (((𝜑 ∧ (𝐴 ∈ (Base‘𝐶) ∧ 𝐵 ∈ (Base‘𝐶))) ∧ (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴))) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
4847exp42 428 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ (Base‘𝐶) → (𝐵 ∈ (Base‘𝐶) → ((∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))))
4948com24 95 . . . . . . . . 9 (𝜑 → ((∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → (𝐵 ∈ (Base‘𝐶) → (𝐴 ∈ (Base‘𝐶) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))))
5049com14 96 . . . . . . . 8 (𝐴 ∈ (Base‘𝐶) → ((∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → (𝐵 ∈ (Base‘𝐶) → (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))))
5150expd 408 . . . . . . 7 (𝐴 ∈ (Base‘𝐶) → (∃!𝑓 𝑓 ∈ (𝐴(Hom ‘𝐶)𝐵) → (∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) → (𝐵 ∈ (Base‘𝐶) → (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))))
5213, 51syldc 48 . . . . . 6 (∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) → (𝐴 ∈ (Base‘𝐶) → (∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) → (𝐵 ∈ (Base‘𝐶) → (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))))
5352com15 101 . . . . 5 (𝜑 → (𝐴 ∈ (Base‘𝐶) → (∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴) → (𝐵 ∈ (Base‘𝐶) → (∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))))
5453impd 402 . . . 4 (𝜑 → ((𝐴 ∈ (Base‘𝐶) ∧ ∀𝑏 ∈ (Base‘𝐶)∃!𝑔 𝑔 ∈ (𝑏(Hom ‘𝐶)𝐴)) → (𝐵 ∈ (Base‘𝐶) → (∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))))
559, 54mpd 15 . . 3 (𝜑 → (𝐵 ∈ (Base‘𝐶) → (∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))))
5655impd 402 . 2 (𝜑 → ((𝐵 ∈ (Base‘𝐶) ∧ ∀𝑎 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (𝑎(Hom ‘𝐶)𝐵)) → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵)))
576, 56mpd 15 1 (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wex 1742  wcel 2048  ∃!weu 2579  wral 3082  wss 3825   class class class wbr 4923  cfv 6182  (class class class)co 6970  Basecbs 16329  Hom chom 16422  Catccat 16783  Invcinv 16863  Isociso 16864  TermOctermo 17097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-1st 7494  df-2nd 7495  df-cat 16787  df-cid 16788  df-sect 16865  df-inv 16866  df-iso 16867  df-termo 17100
This theorem is referenced by:  termoeu1w  17127
  Copyright terms: Public domain W3C validator