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 : \emptyset ⟶ \emptyset\}$
	Assertion	griedg0ssusgr	$⊢ U \subseteq USGraph$

Proof

Step	Hyp	Ref	Expression
1		griedg0prc.u	$⊢ U = \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\}$
2	1	eleq2i	$⊢ g \in U \leftrightarrow g \in \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\}$
3		elopab	$⊢ g \in \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \leftrightarrow \exists v \exists e (g = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset)$
4	2 3	bitri	$⊢ g \in U \leftrightarrow \exists v \exists e (g = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset)$
5		opex	$⊢ ⟨v, e⟩ \in V$
6	5	a1i	$⊢ e : \emptyset ⟶ \emptyset \to ⟨v, e⟩ \in V$
7		vex	$⊢ v \in V$
8		vex	$⊢ e \in V$
9	7 8	opiedgfvi	$⊢ iEdg (⟨v, e⟩) = e$
10		f0bi	$⊢ e : \emptyset ⟶ \emptyset \leftrightarrow e = \emptyset$
11	10	biimpi	$⊢ e : \emptyset ⟶ \emptyset \to e = \emptyset$
12	9 11	eqtrid	$⊢ e : \emptyset ⟶ \emptyset \to iEdg (⟨v, e⟩) = \emptyset$
13	6 12	usgr0e	$⊢ e : \emptyset ⟶ \emptyset \to ⟨v, e⟩ \in USGraph$
14	13	adantl	$⊢ (g = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to ⟨v, e⟩ \in USGraph$
15		eleq1	$⊢ g = ⟨v, e⟩ \to (g \in USGraph \leftrightarrow ⟨v, e⟩ \in USGraph)$
16	15	adantr	$⊢ (g = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to (g \in USGraph \leftrightarrow ⟨v, e⟩ \in USGraph)$
17	14 16	mpbird	$⊢ (g = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to g \in USGraph$
18	17	exlimivv	$⊢ \exists v \exists e (g = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to g \in USGraph$
19	4 18	sylbi	$⊢ g \in U \to g \in USGraph$
20	19	ssriv	$⊢ U \subseteq USGraph$

Metamath Proof Explorer

Theorem griedg0ssusgr

Proof