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 ) |