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

Metamath Proof Explorer

Theorem thinciso

Description: In a thin category, F : X --> Y is an isomorphism iff there is a morphism from Y to X . (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses thincsect.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thinciso.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
thinciso.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
thinciso.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion thinciso ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 thincsect.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 thincsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 thinciso.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 thinciso.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
7 thinciso.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
8 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
9 1 thinccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 2 5 6 8 9 3 4 7 dfiso3 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) )
11 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) )
12 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
13 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝐶 ∈ ThinCat )
14 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝑌 ∈ 𝐵 )
15 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝑋 ∈ 𝐵 )
16 13 2 14 15 8 5 thincsect ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ) )
17 11 12 16 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
18 13 2 15 14 8 5 thincsect ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ) )
19 12 11 18 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 )
20 17 19 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) ∧ ( 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ⊤ ) ) → ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ) )
21 trud ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → ⊤ )
22 21 reximdva0 ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) → ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ⊤ )
23 20 22 reximddv ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) → ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ) )
24 rexn0 ⊢ ( ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ) → ( 𝑌 𝐻 𝑋 ) ≠ ∅ )
25 24 adantl ⊢ ( ( 𝜑 ∧ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) → ( 𝑌 𝐻 𝑋 ) ≠ ∅ )
26 23 25 impbida ⊢ ( 𝜑 → ( ( 𝑌 𝐻 𝑋 ) ≠ ∅ ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) )
27 10 26 bitr4d ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝑌 𝐻 𝑋 ) ≠ ∅ ) )