Metamath Proof Explorer

Theorem isorcl2

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
isorcl2.b ⊢ B = Base C
Assertion isorcl2 ⊢ φ → X ∈ B ∧ Y ∈ B

Proof

Step Hyp Ref Expression
1 isorcl.i ⊢ I = Iso ⁡ C
2 isorcl.f ⊢ φ → F ∈ X I Y
3 isorcl2.b ⊢ B = Base C
4 eqid ⊢ Inv ⁡ C = Inv ⁡ C
5 1 2 isorcl ⊢ φ → C ∈ Cat
6 3 4 5 1 isofval2 ⊢ φ → I = x ∈ B , y ∈ B ⟼ dom ⁡ x Inv ⁡ C y
7 6 oveqd ⊢ φ → X I Y = X x ∈ B , y ∈ B ⟼ dom ⁡ x Inv ⁡ C y Y
8 2 7 eleqtrd ⊢ φ → F ∈ X x ∈ B , y ∈ B ⟼ dom ⁡ x Inv ⁡ C y Y
9 eqid ⊢ x ∈ B , y ∈ B ⟼ dom ⁡ x Inv ⁡ C y = x ∈ B , y ∈ B ⟼ dom ⁡ x Inv ⁡ C y
10 9 elmpocl ⊢ F ∈ X x ∈ B , y ∈ B ⟼ dom ⁡ x Inv ⁡ C y Y → X ∈ B ∧ Y ∈ B
11 8 10 syl ⊢ φ → X ∈ B ∧ Y ∈ B