Metamath Proof Explorer

Theorem termoeu1

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)

Ref Expression
Hypotheses termoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
termoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( TermO ‘ 𝐶 ) )
termoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( TermO ‘ 𝐶 ) )
Assertion termoeu1 ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 termoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 termoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( TermO ‘ 𝐶 ) )
3 termoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( TermO ‘ 𝐶 ) )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 4 5 1 istermoi ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( TermO ‘ 𝐶 ) ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) ) )
7 3 6 mpdan ⊢ ( 𝜑 → ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) ) )
8 4 5 1 istermoi ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( TermO ‘ 𝐶 ) ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
9 2 8 mpdan ⊢ ( 𝜑 → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
10 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) = ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) )
11 10 eleq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) ↔ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) )
12 11 eubidv ⊢ ( 𝑎 = 𝐴 → ( ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) )
13 12 rspcv ⊢ ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) )
14 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
15 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
18 4 5 14 15 16 17 isohom ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ⊆ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) ) → ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ⊆ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) )
20 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) )
21 20 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) )
22 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) = ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
23 22 eleq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ↔ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
24 23 eubidv ⊢ ( 𝑏 = 𝐵 → ( ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ↔ ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
25 24 rspcva ⊢ ( ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
26 euex ⊢ ( ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
27 25 26 syl ⊢ ( ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
28 27 ex ⊢ ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
29 28 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
30 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
31 15 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) ∧ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐶 ∈ Cat )
32 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) ∧ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
33 17 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) ∧ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
34 1 2 3 2termoinv ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝑓 ( 𝐴 ( Inv ‘ 𝐶 ) 𝐵 ) 𝑔 )
35 34 ad4ant134 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) ∧ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝑓 ( 𝐴 ( Inv ‘ 𝐶 ) 𝐵 ) 𝑔 )
36 4 30 31 32 33 14 35 inviso1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) ∧ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
37 36 ex ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ( 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
38 37 eximdv ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
39 38 expcom ⊢ ( 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) → ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) )
40 39 exlimiv ⊢ ( ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) → ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) )
41 40 com3l ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ( ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) )
42 41 impd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
43 21 29 42 syl2and ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
44 43 imp ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
45 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) )
46 euelss ⊢ ( ( ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ⊆ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
47 19 44 45 46 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
48 47 exp42 ⊢ ( 𝜑 → ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) )
49 48 com24 ⊢ ( 𝜑 → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) )
50 49 com14 ⊢ ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) )
51 50 expd ⊢ ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) ) )
52 13 51 syldc ⊢ ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) ) )
53 52 com15 ⊢ ( 𝜑 → ( 𝐴 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) ) )
54 53 impd ⊢ ( 𝜑 → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝑏 ( Hom ‘ 𝐶 ) 𝐴 ) ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) ) )
55 9 54 mpd ⊢ ( 𝜑 → ( 𝐵 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) ) )
56 55 impd ⊢ ( 𝜑 → ( ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
57 7 56 mpd ⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )