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	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ UPGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ )
2		simplr	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑋 )
3		simprl	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
4		simpl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → 𝑉 ∈ 𝑊 )
5		snex	⊢ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V
6	5	a1i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V )
7		opvtxfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = 𝑉 )
8	4 6 7	syl2an	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = 𝑉 )
9	3 8	eleqtrrd	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) )
10		simprr	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
11	10 8	eleqtrrd	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) )
12		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
13	4 6 12	syl2an	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
14	1 2 9 11 13	upgr1e	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ UPGraph )