This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )