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

Metamath Proof Explorer

Theorem isorcl

Description: Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses isorcl.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
isorcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion isorcl ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 isorcl.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
2 isorcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
3 elfvne0 ⊢ ( 𝐹 ∈ ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → 𝐼 ≠ ∅ )
4 df-ov ⊢ ( 𝑋 𝐼 𝑌 ) = ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5 3 4 eleq2s ⊢ ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) → 𝐼 ≠ ∅ )
6 1 neeq1i ⊢ ( 𝐼 ≠ ∅ ↔ ( Iso ‘ 𝐶 ) ≠ ∅ )
7 n0 ⊢ ( ( Iso ‘ 𝐶 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Iso ‘ 𝐶 ) )
8 6 7 bitri ⊢ ( 𝐼 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Iso ‘ 𝐶 ) )
9 5 8 sylib ⊢ ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) → ∃ 𝑥 𝑥 ∈ ( Iso ‘ 𝐶 ) )
10 df-iso ⊢ Iso = ( 𝑐 ∈ Cat ↦ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) ) )
11 10 mptrcl ⊢ ( 𝑥 ∈ ( Iso ‘ 𝐶 ) → 𝐶 ∈ Cat )
12 11 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( Iso ‘ 𝐶 ) → 𝐶 ∈ Cat )
13 2 9 12 3syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )