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

Metamath Proof Explorer

Theorem thinccic

Description: In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses thincsect.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thinciso.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion thinccic ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 thincsect.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 thincsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 thinciso.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
7 1 thinccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 2 5 6 7 3 4 isohom ⊢ ( 𝜑 → ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )
9 8 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ ThinCat )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑋 ∈ 𝐵 )
12 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑌 ∈ 𝐵 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
14 10 2 11 12 5 6 13 thinciso ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) )
15 9 14 biadanid ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ) )
16 15 exbidv ⊢ ( 𝜑 → ( ∃ 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ) )
17 6 2 7 3 4 cic ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
18 n0 ⊢ ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
19 18 anbi1i ⊢ ( ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) )
20 19.41v ⊢ ( ∃ 𝑓 ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) )
21 19 20 bitr4i ⊢ ( ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) )
22 21 a1i ⊢ ( 𝜑 → ( ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ) )
23 16 17 22 3bitr4d ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ) )