uspgr1ewop

Description: A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021)

		Ref	Expression
	Assertion	uspgr1ewop	$⊢ (V \in W \land A \in V \land B \in V) \to ⟨V, ⟨“ \{A, B\} ”⟩⟩ \in USHGraph$

Step	Hyp	Ref	Expression
1		prex	$⊢ \{A, B\} \in V$
2		s1val	$⊢ \{A, B\} \in V \to ⟨“ \{A, B\} ”⟩ = \{⟨0, \{A, B\}⟩\}$
3	1 2	mp1i	$⊢ (V \in W \land A \in V \land B \in V) \to ⟨“ \{A, B\} ”⟩ = \{⟨0, \{A, B\}⟩\}$
4	3	opeq2d	$⊢ (V \in W \land A \in V \land B \in V) \to ⟨V, ⟨“ \{A, B\} ”⟩⟩ = ⟨V, \{⟨0, \{A, B\}⟩\}⟩$
5		simp1	$⊢ (V \in W \land A \in V \land B \in V) \to V \in W$
6		c0ex	$⊢ 0 \in V$
7	6	a1i	$⊢ (V \in W \land A \in V \land B \in V) \to 0 \in V$
8		3simpc	$⊢ (V \in W \land A \in V \land B \in V) \to (A \in V \land B \in V)$
9		uspgr1eop	$⊢ ((V \in W \land 0 \in V) \land (A \in V \land B \in V)) \to ⟨V, \{⟨0, \{A, B\}⟩\}⟩ \in USHGraph$
10	5 7 8 9	syl21anc	$⊢ (V \in W \land A \in V \land B \in V) \to ⟨V, \{⟨0, \{A, B\}⟩\}⟩ \in USHGraph$
11	4 10	eqeltrd	$⊢ (V \in W \land A \in V \land B \in V) \to ⟨V, ⟨“ \{A, B\} ”⟩⟩ \in USHGraph$

Metamath Proof Explorer