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

Metamath Proof Explorer

Theorem griedg0ssusgr

Description: The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020)

Ref Expression
Hypothesis griedg0prc.u ⊢ U = v e | e : ∅ ⟶ ∅
Assertion griedg0ssusgr ⊢ U ⊆ USGraph

Proof

Step Hyp Ref Expression
1 griedg0prc.u ⊢ U = v e | e : ∅ ⟶ ∅
2 1 eleq2i ⊢ g ∈ U ↔ g ∈ v e | e : ∅ ⟶ ∅
3 elopab ⊢ g ∈ v e | e : ∅ ⟶ ∅ ↔ ∃ v ∃ e g = v e ∧ e : ∅ ⟶ ∅
4 2 3 bitri ⊢ g ∈ U ↔ ∃ v ∃ e g = v e ∧ e : ∅ ⟶ ∅
5 opex ⊢ v e ∈ V
6 5 a1i ⊢ e : ∅ ⟶ ∅ → v e ∈ V
7 vex ⊢ v ∈ V
8 vex ⊢ e ∈ V
9 7 8 opiedgfvi ⊢ iEdg ⁡ v e = e
10 f0bi ⊢ e : ∅ ⟶ ∅ ↔ e = ∅
11 10 biimpi ⊢ e : ∅ ⟶ ∅ → e = ∅
12 9 11 eqtrid ⊢ e : ∅ ⟶ ∅ → iEdg ⁡ v e = ∅
13 6 12 usgr0e ⊢ e : ∅ ⟶ ∅ → v e ∈ USGraph
14 13 adantl ⊢ g = v e ∧ e : ∅ ⟶ ∅ → v e ∈ USGraph
15 eleq1 ⊢ g = v e → g ∈ USGraph ↔ v e ∈ USGraph
16 15 adantr ⊢ g = v e ∧ e : ∅ ⟶ ∅ → g ∈ USGraph ↔ v e ∈ USGraph
17 14 16 mpbird ⊢ g = v e ∧ e : ∅ ⟶ ∅ → g ∈ USGraph
18 17 exlimivv ⊢ ∃ v ∃ e g = v e ∧ e : ∅ ⟶ ∅ → g ∈ USGraph
19 4 18 sylbi ⊢ g ∈ U → g ∈ USGraph
20 19 ssriv ⊢ U ⊆ USGraph