Metamath Proof Explorer

Theorem uspgr1eop

Description: A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

		Ref	Expression
	Assertion	uspgr1eop	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to ⟨V, \{⟨A, \{B, C\}⟩\}⟩ \in USHGraph$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (⟨V, \{⟨A, \{B, C\}⟩\}⟩) = Vtx (⟨V, \{⟨A, \{B, C\}⟩\}⟩)$
2		simplr	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to A \in X$
3		simprl	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to B \in V$
4		simpl	$⊢ (V \in W \land A \in X) \to V \in W$
5		snex	$⊢ \{⟨A, \{B, C\}⟩\} \in V$
6	5	a1i	$⊢ (B \in V \land C \in V) \to \{⟨A, \{B, C\}⟩\} \in V$
7		opvtxfv	$⊢ (V \in W \land \{⟨A, \{B, C\}⟩\} \in V) \to Vtx (⟨V, \{⟨A, \{B, C\}⟩\}⟩) = V$
8	4 6 7	syl2an	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to Vtx (⟨V, \{⟨A, \{B, C\}⟩\}⟩) = V$
9	3 8	eleqtrrd	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to B \in Vtx (⟨V, \{⟨A, \{B, C\}⟩\}⟩)$
10		simprr	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to C \in V$
11	10 8	eleqtrrd	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to C \in Vtx (⟨V, \{⟨A, \{B, C\}⟩\}⟩)$
12		opiedgfv	$⊢ (V \in W \land \{⟨A, \{B, C\}⟩\} \in V) \to iEdg (⟨V, \{⟨A, \{B, C\}⟩\}⟩) = \{⟨A, \{B, C\}⟩\}$
13	4 6 12	syl2an	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to iEdg (⟨V, \{⟨A, \{B, C\}⟩\}⟩) = \{⟨A, \{B, C\}⟩\}$
14	1 2 9 11 13	uspgr1e	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to ⟨V, \{⟨A, \{B, C\}⟩\}⟩ \in USHGraph$