Metamath Proof Explorer

Theorem evth2f

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

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

Proof

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