Metamath Proof Explorer


Theorem evthf

Description: A version of evth using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses evthf.1
|- F/_ x F
evthf.2
|- F/_ y F
evthf.3
|- F/_ x X
evthf.4
|- F/_ y X
evthf.5
|- F/ x ph
evthf.6
|- F/ y ph
evthf.7
|- X = U. J
evthf.8
|- K = ( topGen ` ran (,) )
evthf.9
|- ( ph -> J e. Comp )
evthf.10
|- ( ph -> F e. ( J Cn K ) )
evthf.11
|- ( ph -> X =/= (/) )
Assertion evthf
|- ( ph -> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) )

Proof

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