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 )