Metamath Proof Explorer

Theorem gricrcl

Description: Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025)

Ref Expression
Assertion gricrcl ⊢ G ≃ 𝑔𝑟 S → G ∈ V ∧ S ∈ V

Proof

Step Hyp Ref Expression
1 brgric ⊢ G ≃ 𝑔𝑟 S ↔ G GraphIso S ≠ ∅
2 grimdmrel ⊢ Rel ⁡ dom ⁡ GraphIso
3 2 ovprc ⊢ ¬ G ∈ V ∧ S ∈ V → G GraphIso S = ∅
4 3 necon1ai ⊢ G GraphIso S ≠ ∅ → G ∈ V ∧ S ∈ V
5 1 4 sylbi ⊢ G ≃ 𝑔𝑟 S → G ∈ V ∧ S ∈ V