Step |
Hyp |
Ref |
Expression |
1 |
|
evthf.1 |
|- F/_ x F |
2 |
|
evthf.2 |
|- F/_ y F |
3 |
|
evthf.3 |
|- F/_ x X |
4 |
|
evthf.4 |
|- F/_ y X |
5 |
|
evthf.5 |
|- F/ x ph |
6 |
|
evthf.6 |
|- F/ y ph |
7 |
|
evthf.7 |
|- X = U. J |
8 |
|
evthf.8 |
|- K = ( topGen ` ran (,) ) |
9 |
|
evthf.9 |
|- ( ph -> J e. Comp ) |
10 |
|
evthf.10 |
|- ( ph -> F e. ( J Cn K ) ) |
11 |
|
evthf.11 |
|- ( ph -> X =/= (/) ) |
12 |
7 8 9 10 11
|
evth |
|- ( ph -> E. a e. X A. b e. X ( F ` b ) <_ ( F ` a ) ) |
13 |
|
nfcv |
|- F/_ b X |
14 |
|
nfcv |
|- F/_ y b |
15 |
2 14
|
nffv |
|- F/_ y ( F ` b ) |
16 |
|
nfcv |
|- F/_ y <_ |
17 |
|
nfcv |
|- F/_ y a |
18 |
2 17
|
nffv |
|- F/_ y ( F ` a ) |
19 |
15 16 18
|
nfbr |
|- F/ y ( F ` b ) <_ ( F ` a ) |
20 |
|
nfv |
|- F/ b ( F ` y ) <_ ( F ` a ) |
21 |
|
fveq2 |
|- ( b = y -> ( F ` b ) = ( F ` y ) ) |
22 |
21
|
breq1d |
|- ( b = y -> ( ( F ` b ) <_ ( F ` a ) <-> ( F ` y ) <_ ( F ` a ) ) ) |
23 |
13 4 19 20 22
|
cbvralfw |
|- ( A. b e. X ( F ` b ) <_ ( F ` a ) <-> A. y e. X ( F ` y ) <_ ( F ` a ) ) |
24 |
23
|
rexbii |
|- ( E. a e. X A. b e. X ( F ` b ) <_ ( F ` a ) <-> E. a e. X A. y e. X ( F ` y ) <_ ( F ` a ) ) |
25 |
|
nfcv |
|- F/_ a X |
26 |
|
nfcv |
|- F/_ x y |
27 |
1 26
|
nffv |
|- F/_ x ( F ` y ) |
28 |
|
nfcv |
|- F/_ x <_ |
29 |
|
nfcv |
|- F/_ x a |
30 |
1 29
|
nffv |
|- F/_ x ( F ` a ) |
31 |
27 28 30
|
nfbr |
|- F/ x ( F ` y ) <_ ( F ` a ) |
32 |
3 31
|
nfralw |
|- F/ x A. y e. X ( F ` y ) <_ ( F ` a ) |
33 |
|
nfv |
|- F/ a A. y e. X ( F ` y ) <_ ( F ` x ) |
34 |
|
fveq2 |
|- ( a = x -> ( F ` a ) = ( F ` x ) ) |
35 |
34
|
breq2d |
|- ( a = x -> ( ( F ` y ) <_ ( F ` a ) <-> ( F ` y ) <_ ( F ` x ) ) ) |
36 |
35
|
ralbidv |
|- ( a = x -> ( A. y e. X ( F ` y ) <_ ( F ` a ) <-> A. y e. X ( F ` y ) <_ ( F ` x ) ) ) |
37 |
25 3 32 33 36
|
cbvrexfw |
|- ( E. a e. X A. y e. X ( F ` y ) <_ ( F ` a ) <-> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) ) |
38 |
24 37
|
bitri |
|- ( E. a e. X A. b e. X ( F ` b ) <_ ( F ` a ) <-> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) ) |
39 |
12 38
|
sylib |
|- ( ph -> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) ) |