This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uobeqterm

Description: Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses uobeqterm.a ⊢ A = Base D
uobeqterm.b ⊢ B = Base E
uobeqterm.x ⊢ φ → X ∈ A
uobeqterm.y ⊢ φ → Y ∈ B
uobeqterm.f ⊢ φ → F ∈ C Func D
uobeqterm.g ⊢ φ → G ∈ C Func E
uobeqterm.d No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
uobeqterm.e No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
Assertion uobeqterm Could not format assertion : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 uobeqterm.a ⊢ A = Base D
2 uobeqterm.b ⊢ B = Base E
3 uobeqterm.x ⊢ φ → X ∈ A
4 uobeqterm.y ⊢ φ → Y ∈ B
5 uobeqterm.f ⊢ φ → F ∈ C Func D
6 uobeqterm.g ⊢ φ → G ∈ C Func E
7 uobeqterm.d Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
8 uobeqterm.e Could not format ( ph -> E e. TermCat ) : No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
9 eqid ⊢ CatCat ⁡ D E = CatCat ⁡ D E
10 eqid ⊢ Base CatCat ⁡ D E = Base CatCat ⁡ D E
11 prid1g Could not format ( D e. TermCat -> D e. { D , E } ) : No typesetting found for |- ( D e. TermCat -> D e. { D , E } ) with typecode |-
12 7 11 syl ⊢ φ → D ∈ D E
13 7 termccd ⊢ φ → D ∈ Cat
14 12 13 elind ⊢ φ → D ∈ D E ∩ Cat
15 prex ⊢ D E ∈ V
16 15 a1i ⊢ φ → D E ∈ V
17 9 10 16 catcbas ⊢ φ → Base CatCat ⁡ D E = D E ∩ Cat
18 14 17 eleqtrrd ⊢ φ → D ∈ Base CatCat ⁡ D E
19 prid2g Could not format ( E e. TermCat -> E e. { D , E } ) : No typesetting found for |- ( E e. TermCat -> E e. { D , E } ) with typecode |-
20 8 19 syl ⊢ φ → E ∈ D E
21 8 termccd ⊢ φ → E ∈ Cat
22 20 21 elind ⊢ φ → E ∈ D E ∩ Cat
23 22 17 eleqtrrd ⊢ φ → E ∈ Base CatCat ⁡ D E
24 9 10 18 23 7 termcciso Could not format ( ph -> ( E e. TermCat <-> D ( ~=c ` ( CatCat ` { D , E } ) ) E ) ) : No typesetting found for |- ( ph -> ( E e. TermCat <-> D ( ~=c ` ( CatCat ` { D , E } ) ) E ) ) with typecode |-
25 8 24 mpbid ⊢ φ → D ≃ 𝑐 ⁡ CatCat ⁡ D E E
26 eqid ⊢ Iso ⁡ CatCat ⁡ D E = Iso ⁡ CatCat ⁡ D E
27 9 catccat ⊢ D E ∈ V → CatCat ⁡ D E ∈ Cat
28 16 27 syl ⊢ φ → CatCat ⁡ D E ∈ Cat
29 26 10 28 18 23 cic ⊢ φ → D ≃ 𝑐 ⁡ CatCat ⁡ D E E ↔ ∃ k k ∈ D Iso ⁡ CatCat ⁡ D E E
30 25 29 mpbid ⊢ φ → ∃ k k ∈ D Iso ⁡ CatCat ⁡ D E E
31 3 adantr ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → X ∈ A
32 5 adantr ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → F ∈ C Func D
33 fullfunc ⊢ D Full E ⊆ D Func E
34 simpr ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → k ∈ D Iso ⁡ CatCat ⁡ D E E
35 9 1 2 26 34 catcisoi ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → k ∈ D Full E ∩ D Faith E ∧ 1 st ⁡ k : A ⟶ 1-1 onto B
36 35 simpld ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → k ∈ D Full E ∩ D Faith E
37 36 elin1d ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → k ∈ D Full E
38 33 37 sselid ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → k ∈ D Func E
39 6 adantr ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → G ∈ C Func E
40 8 adantr Could not format ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> E e. TermCat ) : No typesetting found for |- ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> E e. TermCat ) with typecode |-
41 32 38 39 40 cofuterm ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → k ∘ func F = G
42 38 func1st2nd ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → 1 st ⁡ k D Func E 2 nd ⁡ k
43 1 2 42 funcf1 ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → 1 st ⁡ k : A ⟶ B
44 43 31 ffvelcdmd ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → 1 st ⁡ k ⁡ X ∈ B
45 4 adantr ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → Y ∈ B
46 40 2 44 45 termcbasmo ⊢ φ ∧ k ∈ D Iso ⁡ CatCat ⁡ D E E → 1 st ⁡ k ⁡ X = Y
47 1 31 32 41 46 9 26 34 uobeq3 Could not format ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-
48 30 47 exlimddv Could not format ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-