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

Metamath Proof Explorer

Theorem termoeu1w

Description: Terminal objects are essentially unique (weak form), i.e. if A and B are terminal objects, then A and B are isomorphic. Proposition 7.6 of Adamek p. 103. (Contributed by AV, 18-Apr-2020)

		Ref	Expression
	Hypotheses	termoeu1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
		termoeu1.a	⊢ ( 𝜑 → 𝐴 ∈ ( TermO ‘ 𝐶 ) )
		termoeu1.b	⊢ ( 𝜑 → 𝐵 ∈ ( TermO ‘ 𝐶 ) )
	Assertion	termoeu1w	⊢ ( 𝜑 → 𝐴 ( ≃_𝑐 ‘ 𝐶 ) 𝐵 )

Proof

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