Step |
Hyp |
Ref |
Expression |
1 |
|
usgrnloopv.e |
|- E = ( iEdg ` G ) |
2 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
3 |
1 2
|
usgredgprv |
|- ( ( G e. USGraph /\ x e. dom E ) -> ( ( E ` x ) = { M , N } -> ( M e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) ) |
4 |
3
|
imp |
|- ( ( ( G e. USGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> ( M e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) |
5 |
1
|
usgrnloopv |
|- ( ( G e. USGraph /\ M e. ( Vtx ` G ) ) -> ( ( E ` x ) = { M , N } -> M =/= N ) ) |
6 |
5
|
ex |
|- ( G e. USGraph -> ( M e. ( Vtx ` G ) -> ( ( E ` x ) = { M , N } -> M =/= N ) ) ) |
7 |
6
|
com23 |
|- ( G e. USGraph -> ( ( E ` x ) = { M , N } -> ( M e. ( Vtx ` G ) -> M =/= N ) ) ) |
8 |
7
|
adantr |
|- ( ( G e. USGraph /\ x e. dom E ) -> ( ( E ` x ) = { M , N } -> ( M e. ( Vtx ` G ) -> M =/= N ) ) ) |
9 |
8
|
imp |
|- ( ( ( G e. USGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> ( M e. ( Vtx ` G ) -> M =/= N ) ) |
10 |
9
|
com12 |
|- ( M e. ( Vtx ` G ) -> ( ( ( G e. USGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> M =/= N ) ) |
11 |
10
|
adantr |
|- ( ( M e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) -> ( ( ( G e. USGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> M =/= N ) ) |
12 |
4 11
|
mpcom |
|- ( ( ( G e. USGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> M =/= N ) |
13 |
12
|
ex |
|- ( ( G e. USGraph /\ x e. dom E ) -> ( ( E ` x ) = { M , N } -> M =/= N ) ) |
14 |
13
|
rexlimdva |
|- ( G e. USGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) ) |