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

Metamath Proof Explorer

Theorem initoeu2

Description: Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in Adamek p. 102. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
initoeu2.i ⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )
Assertion initoeu2 ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3 initoeu2.i ⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )
4 ciclcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
5 1 4 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
6 cicrcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
7 1 6 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
9 cicsym ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐵 ( ≃𝑐 ‘ 𝐶 ) 𝐴 )
10 8 9 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐵 ( ≃𝑐 ‘ 𝐶 ) 𝐴 )
11 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
15 11 12 8 13 14 cic ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐵 ( ≃𝑐 ‘ 𝐶 ) 𝐴 ↔ ∃ 𝑘 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) )
16 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17 12 16 1 isinitoi ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ) )
18 2 17 mpdan ⊢ ( 𝜑 → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ) )
19 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) = ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) )
20 19 eleq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ↔ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
21 20 eubidv ⊢ ( 𝑎 = 𝑏 → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
22 21 rspcva ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) )
23 nfv ⊢ Ⅎ ℎ 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 )
24 nfv ⊢ Ⅎ 𝑓 ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 )
25 eleq1w ⊢ ( 𝑓 = ℎ → ( 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ↔ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
26 23 24 25 cbveuw ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ↔ ∃! ℎ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) )
27 euex ⊢ ( ∃! ℎ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃ ℎ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
29 simpr ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
30 29 ad2antrl ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
31 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
32 12 16 11 28 30 31 isohom ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ⊆ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
33 32 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) → 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
34 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
35 28 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → 𝐶 ∈ Cat )
36 30 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
37 31 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
38 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑏 ∈ ( Base ‘ 𝐶 ) )
39 38 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → 𝑏 ∈ ( Base ‘ 𝐶 ) )
40 simprl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
41 simprr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) )
42 12 16 34 35 36 37 39 40 41 catcocl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) )
43 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) → 𝜑 )
44 df-3an ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ↔ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) )
45 44 biimpri ⊢ ( ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) )
46 45 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) → ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) )
47 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) → 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) )
48 47 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) → 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) )
49 41 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) → ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) )
50 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) → ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) )
51 1 2 12 16 11 34 initoeu2lem2 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
52 43 46 48 49 50 51 syl113anc ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ∧ ( ℎ ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑘 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
53 42 52 mpdan ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) ∧ ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
54 53 ex ⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) → ( ( 𝑘 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) )
55 33 54 mpand ⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) )
56 55 ex ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) )
57 56 com23 ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) )
58 57 ex ⊢ ( 𝜑 → ( ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
59 58 com15 ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
60 59 expd ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) ) )
61 60 com24 ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) ) )
62 61 com12 ⊢ ( ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) ) )
63 62 exlimiv ⊢ ( ∃ ℎ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) ) )
64 27 63 syl ⊢ ( ∃! ℎ ℎ ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) ) )
65 26 64 sylbi ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) ) )
66 65 pm2.43i ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
67 66 com12 ⊢ ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
68 67 adantr ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑏 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
69 22 68 mpd ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) )
70 69 ex ⊢ ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝜑 → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
71 70 com15 ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
72 71 adantld ⊢ ( 𝜑 → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) ) )
73 18 72 mpd ⊢ ( 𝜑 → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) ) )
74 73 imp ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) )
75 74 exlimdv ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑘 𝑘 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) )
76 15 75 sylbid ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐵 ( ≃𝑐 ‘ 𝐶 ) 𝐴 → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → ( 𝐵 ( ≃𝑐 ‘ 𝐶 ) 𝐴 → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) )
78 10 77 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
79 78 an32s ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑏 ∈ ( Base ‘ 𝐶 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
80 79 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) )
81 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
82 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
83 12 16 81 82 isinito ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐵 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! 𝑔 𝑔 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
84 80 83 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) ∧ ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
85 84 ex ⊢ ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → ( ( 𝐴 ∈ ( Base ‘ 𝐶 ) ∧ 𝐵 ∈ ( Base ‘ 𝐶 ) ) → 𝐵 ∈ ( InitO ‘ 𝐶 ) ) )
86 5 7 85 mp2and ⊢ ( ( 𝜑 ∧ 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ) → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
87 3 86 mpdan ⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )