Metamath Proof Explorer

Theorem initoeu1

Description: Initial objects are essentially unique (strong form), i.e. there is a unique isomorphism between two initial 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, 14-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3 initoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 4 5 1 isinitoi ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
7 2 6 mpdan ⊢ ( 𝜑 → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
8 4 5 1 isinitoi ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑎 ) ) )
9 3 8 mpdan ⊢ ( 𝜑 → ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑎 ) ) )
10 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 ( 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 simprr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ 𝐴 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ( 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 oveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐵 ( 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 2initoinv ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐵 ( 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 ‘ 𝐶 ) 𝐵 ) )