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	syl5eq	⊢ ( 𝑒 : ∅ ⟶ ∅ → ( 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