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 ‘ 𝐶 ) 𝐵 ) )