Metamath Proof Explorer

Theorem upgr1eop

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 10-Oct-2020)

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

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	upgr1e	$⊢ ((V \in W \land A \in X) \land (B \in V \land C \in V)) \to ⟨V, \{⟨A, \{B, C\}⟩\}⟩ \in UPGraph$