Theorem usgr2v1e2w

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

	Ref	Expression
Assertion	usgr2v1e2w	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ⟨ { 𝐴 , 𝐵 } , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		prex	⊢ { 𝐴 , 𝐵 } ∈ V
2		s1val	⊢ ( { 𝐴 , 𝐵 } ∈ V → ⟨“ { 𝐴 , 𝐵 } ”⟩ = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } )
3	1 2	mp1i	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ⟨“ { 𝐴 , 𝐵 } ”⟩ = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } )
4	3	opeq2d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ⟨ { 𝐴 , 𝐵 } , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ = ⟨ { 𝐴 , 𝐵 } , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ )
5		prid1g	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 , 𝐵 } )
6		prid2g	⊢ ( 𝐵 ∈ 𝑌 → 𝐵 ∈ { 𝐴 , 𝐵 } )
7	5 6	anim12i	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) )
8		c0ex	⊢ 0 ∈ V
9	1 8	pm3.2i	⊢ ( { 𝐴 , 𝐵 } ∈ V ∧ 0 ∈ V )
10	7 9	jctil	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( { 𝐴 , 𝐵 } ∈ V ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) )
11		usgr1eop	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ V ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) → ( 𝐴 ≠ 𝐵 → ⟨ { 𝐴 , 𝐵 } , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USGraph ) )
12	11	imp	⊢ ( ( ( ( { 𝐴 , 𝐵 } ∈ V ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) ∧ 𝐴 ≠ 𝐵 ) → ⟨ { 𝐴 , 𝐵 } , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USGraph )
13	10 12	stoic3	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ⟨ { 𝐴 , 𝐵 } , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USGraph )
14	4 13	eqeltrd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ⟨ { 𝐴 , 𝐵 } , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USGraph )