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