Theorem 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	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨ 𝑉 , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )

Proof

Step	Hyp	Ref	Expression
1		prex	⊢ { 𝐴 , 𝐵 } ∈ V
2		s1val	⊢ ( { 𝐴 , 𝐵 } ∈ V → ⟨“ { 𝐴 , 𝐵 } ”⟩ = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } )
3	1 2	mp1i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨“ { 𝐴 , 𝐵 } ”⟩ = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } )
4	3	opeq2d	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨ 𝑉 , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ )
5		simp1	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑉 ∈ 𝑊 )
6		c0ex	⊢ 0 ∈ V
7	6	a1i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 0 ∈ V )
8		3simpc	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
9		uspgr1eop	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USPGraph )
10	5 7 8 9	syl21anc	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USPGraph )
11	4 10	eqeltrd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨ 𝑉 , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )