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→AB⟨“AB”⟩∈USGraph

Proof

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