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 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B ⟨“ A B ”⟩ ∈ USGraph

Proof

Step Hyp Ref Expression
1 prex ⊢ A B ∈ V
2 s1val ⊢ A B ∈ V → ⟨“ A B ”⟩ = 0 A B
3 1 2 mp1i ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → ⟨“ A B ”⟩ = 0 A B
4 3 opeq2d ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B ⟨“ A B ”⟩ = A B 0 A B
5 prid1g ⊢ A ∈ X → A ∈ A B
6 prid2g ⊢ B ∈ Y → B ∈ A B
7 5 6 anim12i ⊢ A ∈ X ∧ B ∈ Y → A ∈ A B ∧ B ∈ A B
8 c0ex ⊢ 0 ∈ V
9 1 8 pm3.2i ⊢ A B ∈ V ∧ 0 ∈ V
10 7 9 jctil ⊢ A ∈ X ∧ B ∈ Y → A B ∈ V ∧ 0 ∈ V ∧ A ∈ A B ∧ B ∈ A B
11 usgr1eop ⊢ A B ∈ V ∧ 0 ∈ V ∧ A ∈ A B ∧ B ∈ A B → A ≠ B → A B 0 A B ∈ USGraph
12 11 imp ⊢ A B ∈ V ∧ 0 ∈ V ∧ A ∈ A B ∧ B ∈ A B ∧ A ≠ B → A B 0 A B ∈ USGraph
13 10 12 stoic3 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B 0 A B ∈ USGraph
14 4 13 eqeltrd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B ⟨“ A B ”⟩ ∈ USGraph