Theorem initoeu1w

Description: Initial objects are essentially unique (weak form), i.e. if A and B are initial objects, then A and B are isomorphic. Proposition 7.3 (1) of Adamek p. 102. (Contributed by AV, 6-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		initoeu1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		initoeu1.a	⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3		initoeu1.b	⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
4	1 2 3	initoeu1	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
5		euex	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
6	4 5	syl	⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
7		eqid	⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		initoo	⊢ ( 𝐶 ∈ Cat → ( 𝐴 ∈ ( InitO ‘ 𝐶 ) → 𝐴 ∈ ( Base ‘ 𝐶 ) ) )
10	1 2 9	sylc	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐶 ) )
11		initoo	⊢ ( 𝐶 ∈ Cat → ( 𝐵 ∈ ( InitO ‘ 𝐶 ) → 𝐵 ∈ ( Base ‘ 𝐶 ) ) )
12	1 3 11	sylc	⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ 𝐶 ) )
13	7 8 1 10 12	cic	⊢ ( 𝜑 → ( 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
14	6 13	mpbird	⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )