Metamath Proof Explorer

Theorem isorcl

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

Ref Expression
Hypotheses isorcl.i ⊢ I = Iso ⁡ C
isorcl.f ⊢ φ → F ∈ X I Y
Assertion isorcl ⊢ φ → C ∈ Cat

Proof

Step Hyp Ref Expression
1 isorcl.i ⊢ I = Iso ⁡ C
2 isorcl.f ⊢ φ → F ∈ X I Y
3 elfvne0 ⊢ F ∈ I ⁡ X Y → I ≠ ∅
4 df-ov ⊢ X I Y = I ⁡ X Y
5 3 4 eleq2s ⊢ F ∈ X I Y → I ≠ ∅
6 1 neeq1i ⊢ I ≠ ∅ ↔ Iso ⁡ C ≠ ∅
7 n0 ⊢ Iso ⁡ C ≠ ∅ ↔ ∃ x x ∈ Iso ⁡ C
8 6 7 bitri ⊢ I ≠ ∅ ↔ ∃ x x ∈ Iso ⁡ C
9 5 8 sylib ⊢ F ∈ X I Y → ∃ x x ∈ Iso ⁡ C
10 df-iso ⊢ Iso = c ∈ Cat ⟼ x ∈ V ⟼ dom ⁡ x ∘ Inv ⁡ c
11 10 mptrcl ⊢ x ∈ Iso ⁡ C → C ∈ Cat
12 11 exlimiv ⊢ ∃ x x ∈ Iso ⁡ C → C ∈ Cat
13 2 9 12 3syl ⊢ φ → C ∈ Cat