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 e. X /\ B e. Y /\ A =/= B ) -> <. { A , B } , <" { A , B } "> >. e. USGraph )

Proof

Step Hyp Ref Expression
1 prex
 |-  { A , B } e. _V
2 s1val
 |-  ( { A , B } e. _V -> <" { A , B } "> = { <. 0 , { A , B } >. } )
3 1 2 mp1i
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> <" { A , B } "> = { <. 0 , { A , B } >. } )
4 3 opeq2d
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> <. { A , B } , <" { A , B } "> >. = <. { A , B } , { <. 0 , { A , B } >. } >. )
5 prid1g
 |-  ( A e. X -> A e. { A , B } )
6 prid2g
 |-  ( B e. Y -> B e. { A , B } )
7 5 6 anim12i
 |-  ( ( A e. X /\ B e. Y ) -> ( A e. { A , B } /\ B e. { A , B } ) )
8 c0ex
 |-  0 e. _V
9 1 8 pm3.2i
 |-  ( { A , B } e. _V /\ 0 e. _V )
10 7 9 jctil
 |-  ( ( A e. X /\ B e. Y ) -> ( ( { A , B } e. _V /\ 0 e. _V ) /\ ( A e. { A , B } /\ B e. { A , B } ) ) )
11 usgr1eop
 |-  ( ( ( { A , B } e. _V /\ 0 e. _V ) /\ ( A e. { A , B } /\ B e. { A , B } ) ) -> ( A =/= B -> <. { A , B } , { <. 0 , { A , B } >. } >. e. USGraph ) )
12 11 imp
 |-  ( ( ( ( { A , B } e. _V /\ 0 e. _V ) /\ ( A e. { A , B } /\ B e. { A , B } ) ) /\ A =/= B ) -> <. { A , B } , { <. 0 , { A , B } >. } >. e. USGraph )
13 10 12 stoic3
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> <. { A , B } , { <. 0 , { A , B } >. } >. e. USGraph )
14 4 13 eqeltrd
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> <. { A , B } , <" { A , B } "> >. e. USGraph )