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 ⊢ 𝑈 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ }
Assertion griedg0ssusgr 𝑈 ⊆ USGraph

Proof

Step Hyp Ref Expression
1 griedg0prc.u ⊢ 𝑈 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ }
2 1 eleq2i ⊢ ( 𝑔 ∈ 𝑈 ↔ 𝑔 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } )
3 elopab ⊢ ( 𝑔 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ↔ ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) )
4 2 3 bitri ⊢ ( 𝑔 ∈ 𝑈 ↔ ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) )
5 opex ⊢ ⟨ 𝑣 , 𝑒 ⟩ ∈ V
6 5 a1i ⊢ ( 𝑒 : ∅ ⟶ ∅ → ⟨ 𝑣 , 𝑒 ⟩ ∈ V )
7 vex ⊢ 𝑣 ∈ V
8 vex ⊢ 𝑒 ∈ V
9 7 8 opiedgfvi ⊢ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = 𝑒
10 f0bi ⊢ ( 𝑒 : ∅ ⟶ ∅ ↔ 𝑒 = ∅ )
11 10 biimpi ⊢ ( 𝑒 : ∅ ⟶ ∅ → 𝑒 = ∅ )
12 9 11 eqtrid ⊢ ( 𝑒 : ∅ ⟶ ∅ → ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ )
13 6 12 usgr0e ⊢ ( 𝑒 : ∅ ⟶ ∅ → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph )
14 13 adantl ⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph )
15 eleq1 ⊢ ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ → ( 𝑔 ∈ USGraph ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) )
16 15 adantr ⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ( 𝑔 ∈ USGraph ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) )
17 14 16 mpbird ⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → 𝑔 ∈ USGraph )
18 17 exlimivv ⊢ ( ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → 𝑔 ∈ USGraph )
19 4 18 sylbi ⊢ ( 𝑔 ∈ 𝑈 → 𝑔 ∈ USGraph )
20 19 ssriv ⊢ 𝑈 ⊆ USGraph