Step |
Hyp |
Ref |
Expression |
1 |
|
isupgr.v |
|- V = ( Vtx ` G ) |
2 |
|
isupgr.e |
|- E = ( iEdg ` G ) |
3 |
1 2
|
upgrn0 |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) =/= (/) ) |
4 |
|
n0 |
|- ( ( E ` F ) =/= (/) <-> E. x x e. ( E ` F ) ) |
5 |
3 4
|
sylib |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x x e. ( E ` F ) ) |
6 |
|
simp1 |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> G e. UPGraph ) |
7 |
|
fndm |
|- ( E Fn A -> dom E = A ) |
8 |
7
|
eqcomd |
|- ( E Fn A -> A = dom E ) |
9 |
8
|
eleq2d |
|- ( E Fn A -> ( F e. A <-> F e. dom E ) ) |
10 |
9
|
biimpd |
|- ( E Fn A -> ( F e. A -> F e. dom E ) ) |
11 |
10
|
a1i |
|- ( G e. UPGraph -> ( E Fn A -> ( F e. A -> F e. dom E ) ) ) |
12 |
11
|
3imp |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> F e. dom E ) |
13 |
1 2
|
upgrss |
|- ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) C_ V ) |
14 |
6 12 13
|
syl2anc |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) C_ V ) |
15 |
14
|
sselda |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> x e. V ) |
16 |
15
|
adantr |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> x e. V ) |
17 |
|
simpr |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> ( ( E ` F ) \ { x } ) = (/) ) |
18 |
|
ssdif0 |
|- ( ( E ` F ) C_ { x } <-> ( ( E ` F ) \ { x } ) = (/) ) |
19 |
17 18
|
sylibr |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> ( E ` F ) C_ { x } ) |
20 |
|
simpr |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> x e. ( E ` F ) ) |
21 |
20
|
snssd |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> { x } C_ ( E ` F ) ) |
22 |
21
|
adantr |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> { x } C_ ( E ` F ) ) |
23 |
19 22
|
eqssd |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> ( E ` F ) = { x } ) |
24 |
|
preq2 |
|- ( y = x -> { x , y } = { x , x } ) |
25 |
|
dfsn2 |
|- { x } = { x , x } |
26 |
24 25
|
eqtr4di |
|- ( y = x -> { x , y } = { x } ) |
27 |
26
|
rspceeqv |
|- ( ( x e. V /\ ( E ` F ) = { x } ) -> E. y e. V ( E ` F ) = { x , y } ) |
28 |
16 23 27
|
syl2anc |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> E. y e. V ( E ` F ) = { x , y } ) |
29 |
|
n0 |
|- ( ( ( E ` F ) \ { x } ) =/= (/) <-> E. y y e. ( ( E ` F ) \ { x } ) ) |
30 |
14
|
adantr |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) C_ V ) |
31 |
|
simprr |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y e. ( ( E ` F ) \ { x } ) ) |
32 |
31
|
eldifad |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y e. ( E ` F ) ) |
33 |
30 32
|
sseldd |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y e. V ) |
34 |
1 2
|
upgrfi |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. Fin ) |
35 |
34
|
adantr |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) e. Fin ) |
36 |
|
simprl |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> x e. ( E ` F ) ) |
37 |
36 32
|
prssd |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } C_ ( E ` F ) ) |
38 |
|
fvex |
|- ( E ` F ) e. _V |
39 |
|
ssdomg |
|- ( ( E ` F ) e. _V -> ( { x , y } C_ ( E ` F ) -> { x , y } ~<_ ( E ` F ) ) ) |
40 |
38 37 39
|
mpsyl |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } ~<_ ( E ` F ) ) |
41 |
1 2
|
upgrle |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( # ` ( E ` F ) ) <_ 2 ) |
42 |
41
|
adantr |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( # ` ( E ` F ) ) <_ 2 ) |
43 |
|
eldifsni |
|- ( y e. ( ( E ` F ) \ { x } ) -> y =/= x ) |
44 |
43
|
ad2antll |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y =/= x ) |
45 |
44
|
necomd |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> x =/= y ) |
46 |
|
hashprg |
|- ( ( x e. _V /\ y e. _V ) -> ( x =/= y <-> ( # ` { x , y } ) = 2 ) ) |
47 |
46
|
el2v |
|- ( x =/= y <-> ( # ` { x , y } ) = 2 ) |
48 |
45 47
|
sylib |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( # ` { x , y } ) = 2 ) |
49 |
42 48
|
breqtrrd |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( # ` ( E ` F ) ) <_ ( # ` { x , y } ) ) |
50 |
|
prfi |
|- { x , y } e. Fin |
51 |
|
hashdom |
|- ( ( ( E ` F ) e. Fin /\ { x , y } e. Fin ) -> ( ( # ` ( E ` F ) ) <_ ( # ` { x , y } ) <-> ( E ` F ) ~<_ { x , y } ) ) |
52 |
35 50 51
|
sylancl |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( ( # ` ( E ` F ) ) <_ ( # ` { x , y } ) <-> ( E ` F ) ~<_ { x , y } ) ) |
53 |
49 52
|
mpbid |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) ~<_ { x , y } ) |
54 |
|
sbth |
|- ( ( { x , y } ~<_ ( E ` F ) /\ ( E ` F ) ~<_ { x , y } ) -> { x , y } ~~ ( E ` F ) ) |
55 |
40 53 54
|
syl2anc |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } ~~ ( E ` F ) ) |
56 |
|
fisseneq |
|- ( ( ( E ` F ) e. Fin /\ { x , y } C_ ( E ` F ) /\ { x , y } ~~ ( E ` F ) ) -> { x , y } = ( E ` F ) ) |
57 |
35 37 55 56
|
syl3anc |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } = ( E ` F ) ) |
58 |
57
|
eqcomd |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) = { x , y } ) |
59 |
33 58
|
jca |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( y e. V /\ ( E ` F ) = { x , y } ) ) |
60 |
59
|
expr |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> ( y e. ( ( E ` F ) \ { x } ) -> ( y e. V /\ ( E ` F ) = { x , y } ) ) ) |
61 |
60
|
eximdv |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> ( E. y y e. ( ( E ` F ) \ { x } ) -> E. y ( y e. V /\ ( E ` F ) = { x , y } ) ) ) |
62 |
61
|
imp |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ E. y y e. ( ( E ` F ) \ { x } ) ) -> E. y ( y e. V /\ ( E ` F ) = { x , y } ) ) |
63 |
|
df-rex |
|- ( E. y e. V ( E ` F ) = { x , y } <-> E. y ( y e. V /\ ( E ` F ) = { x , y } ) ) |
64 |
62 63
|
sylibr |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ E. y y e. ( ( E ` F ) \ { x } ) ) -> E. y e. V ( E ` F ) = { x , y } ) |
65 |
29 64
|
sylan2b |
|- ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) =/= (/) ) -> E. y e. V ( E ` F ) = { x , y } ) |
66 |
28 65
|
pm2.61dane |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> E. y e. V ( E ` F ) = { x , y } ) |
67 |
15 66
|
jca |
|- ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) |
68 |
67
|
ex |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( x e. ( E ` F ) -> ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) ) |
69 |
68
|
eximdv |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E. x x e. ( E ` F ) -> E. x ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) ) |
70 |
5 69
|
mpd |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) |
71 |
|
df-rex |
|- ( E. x e. V E. y e. V ( E ` F ) = { x , y } <-> E. x ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) |
72 |
70 71
|
sylibr |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x e. V E. y e. V ( E ` F ) = { x , y } ) |