Step |
Hyp |
Ref |
Expression |
1 |
|
umgrnloopv.e |
|- E = ( iEdg ` G ) |
2 |
|
prnzg |
|- ( M e. W -> { M , N } =/= (/) ) |
3 |
2
|
adantl |
|- ( ( ( E ` X ) = { M , N } /\ M e. W ) -> { M , N } =/= (/) ) |
4 |
|
neeq1 |
|- ( ( E ` X ) = { M , N } -> ( ( E ` X ) =/= (/) <-> { M , N } =/= (/) ) ) |
5 |
4
|
adantr |
|- ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( ( E ` X ) =/= (/) <-> { M , N } =/= (/) ) ) |
6 |
3 5
|
mpbird |
|- ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( E ` X ) =/= (/) ) |
7 |
|
fvfundmfvn0 |
|- ( ( E ` X ) =/= (/) -> ( X e. dom E /\ Fun ( E |` { X } ) ) ) |
8 |
6 7
|
syl |
|- ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( X e. dom E /\ Fun ( E |` { X } ) ) ) |
9 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
10 |
9 1
|
umgredg2 |
|- ( ( G e. UMGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 ) |
11 |
|
fveqeq2 |
|- ( ( E ` X ) = { M , N } -> ( ( # ` ( E ` X ) ) = 2 <-> ( # ` { M , N } ) = 2 ) ) |
12 |
|
eqid |
|- { M , N } = { M , N } |
13 |
12
|
hashprdifel |
|- ( ( # ` { M , N } ) = 2 -> ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) ) |
14 |
13
|
simp3d |
|- ( ( # ` { M , N } ) = 2 -> M =/= N ) |
15 |
11 14
|
syl6bi |
|- ( ( E ` X ) = { M , N } -> ( ( # ` ( E ` X ) ) = 2 -> M =/= N ) ) |
16 |
15
|
adantr |
|- ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( ( # ` ( E ` X ) ) = 2 -> M =/= N ) ) |
17 |
10 16
|
syl5com |
|- ( ( G e. UMGraph /\ X e. dom E ) -> ( ( ( E ` X ) = { M , N } /\ M e. W ) -> M =/= N ) ) |
18 |
17
|
expcom |
|- ( X e. dom E -> ( G e. UMGraph -> ( ( ( E ` X ) = { M , N } /\ M e. W ) -> M =/= N ) ) ) |
19 |
18
|
com23 |
|- ( X e. dom E -> ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( G e. UMGraph -> M =/= N ) ) ) |
20 |
19
|
adantr |
|- ( ( X e. dom E /\ Fun ( E |` { X } ) ) -> ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( G e. UMGraph -> M =/= N ) ) ) |
21 |
8 20
|
mpcom |
|- ( ( ( E ` X ) = { M , N } /\ M e. W ) -> ( G e. UMGraph -> M =/= N ) ) |
22 |
21
|
ex |
|- ( ( E ` X ) = { M , N } -> ( M e. W -> ( G e. UMGraph -> M =/= N ) ) ) |
23 |
22
|
com13 |
|- ( G e. UMGraph -> ( M e. W -> ( ( E ` X ) = { M , N } -> M =/= N ) ) ) |
24 |
23
|
imp |
|- ( ( G e. UMGraph /\ M e. W ) -> ( ( E ` X ) = { M , N } -> M =/= N ) ) |