Metamath Proof Explorer

Theorem uobeqterm

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

Ref Expression
Hypotheses uobeqterm.a ⊢ 𝐴 = ( Base ‘ 𝐷 )
uobeqterm.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
uobeqterm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
uobeqterm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
uobeqterm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
uobeqterm.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
uobeqterm.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
uobeqterm.e ⊢ ( 𝜑 → 𝐸 ∈ TermCat )
Assertion uobeqterm ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 uobeqterm.a ⊢ 𝐴 = ( Base ‘ 𝐷 )
2 uobeqterm.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
3 uobeqterm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4 uobeqterm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 uobeqterm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6 uobeqterm.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
7 uobeqterm.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
8 uobeqterm.e ⊢ ( 𝜑 → 𝐸 ∈ TermCat )
9 eqid ⊢ ( CatCat ‘ { 𝐷 , 𝐸 } ) = ( CatCat ‘ { 𝐷 , 𝐸 } )
10 eqid ⊢ ( Base ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) = ( Base ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) )
11 prid1g ⊢ ( 𝐷 ∈ TermCat → 𝐷 ∈ { 𝐷 , 𝐸 } )
12 7 11 syl ⊢ ( 𝜑 → 𝐷 ∈ { 𝐷 , 𝐸 } )
13 7 termccatd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
14 12 13 elind ⊢ ( 𝜑 → 𝐷 ∈ ( { 𝐷 , 𝐸 } ∩ Cat ) )
15 prex ⊢ { 𝐷 , 𝐸 } ∈ V
16 15 a1i ⊢ ( 𝜑 → { 𝐷 , 𝐸 } ∈ V )
17 9 10 16 catcbas ⊢ ( 𝜑 → ( Base ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) = ( { 𝐷 , 𝐸 } ∩ Cat ) )
18 14 17 eleqtrrd ⊢ ( 𝜑 → 𝐷 ∈ ( Base ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) )
19 prid2g ⊢ ( 𝐸 ∈ TermCat → 𝐸 ∈ { 𝐷 , 𝐸 } )
20 8 19 syl ⊢ ( 𝜑 → 𝐸 ∈ { 𝐷 , 𝐸 } )
21 8 termccatd ⊢ ( 𝜑 → 𝐸 ∈ Cat )
22 20 21 elind ⊢ ( 𝜑 → 𝐸 ∈ ( { 𝐷 , 𝐸 } ∩ Cat ) )
23 22 17 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ ( Base ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) )
24 9 10 18 23 7 termcciso ⊢ ( 𝜑 → ( 𝐸 ∈ TermCat ↔ 𝐷 ( ≃𝑐 ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) )
25 8 24 mpbid ⊢ ( 𝜑 → 𝐷 ( ≃𝑐 ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 )
26 eqid ⊢ ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) = ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) )
27 9 catccat ⊢ ( { 𝐷 , 𝐸 } ∈ V → ( CatCat ‘ { 𝐷 , 𝐸 } ) ∈ Cat )
28 16 27 syl ⊢ ( 𝜑 → ( CatCat ‘ { 𝐷 , 𝐸 } ) ∈ Cat )
29 26 10 28 18 23 cic ⊢ ( 𝜑 → ( 𝐷 ( ≃𝑐 ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ↔ ∃ 𝑘 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) )
30 25 29 mpbid ⊢ ( 𝜑 → ∃ 𝑘 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) )
31 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝑋 ∈ 𝐴 )
32 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
33 fullfunc ⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) )
35 9 1 2 26 34 catcisoi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → ( 𝑘 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ ( 1st ‘ 𝑘 ) : 𝐴 –1-1-onto→ 𝐵 ) )
36 35 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝑘 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
37 36 elin1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝑘 ∈ ( 𝐷 Full 𝐸 ) )
38 33 37 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝑘 ∈ ( 𝐷 Func 𝐸 ) )
39 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
40 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝐸 ∈ TermCat )
41 32 38 39 40 cofuterm ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → ( 𝑘 ∘func 𝐹 ) = 𝐺 )
42 38 func1st2nd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → ( 1st ‘ 𝑘 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝑘 ) )
43 1 2 42 funcf1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → ( 1st ‘ 𝑘 ) : 𝐴 ⟶ 𝐵 )
44 43 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → ( ( 1st ‘ 𝑘 ) ‘ 𝑋 ) ∈ 𝐵 )
45 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → 𝑌 ∈ 𝐵 )
46 40 2 44 45 termcbasmo ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → ( ( 1st ‘ 𝑘 ) ‘ 𝑋 ) = 𝑌 )
47 1 31 32 41 46 9 26 34 uobeq3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ( Iso ‘ ( CatCat ‘ { 𝐷 , 𝐸 } ) ) 𝐸 ) ) → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )
48 30 47 exlimddv ⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )