Database
BASIC CATEGORY THEORY
Categories
Isomorphic objects
cic
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
⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) )