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

Metamath Proof Explorer

Theorem cic

Description: Objects X and Y in a category are isomorphic provided that there is an isomorphism f : X --> Y , see definition 3.15 of Adamek p. 29. (Contributed by AV, 4-Apr-2020)

Ref Expression
Hypotheses cic.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
cic.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
cic.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
cic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
cic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion cic ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 cic.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
2 cic.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 cic.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 cic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 cic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 1 2 3 4 5 brcic ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ( 𝑋 𝐼 𝑌 ) ≠ ∅ ) )
7 n0 ⊢ ( ( 𝑋 𝐼 𝑌 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
8 6 7 bitrdi ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) )