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 𝑥 𝐹
evth2f.2 𝑦 𝐹
evth2f.3 𝑥 𝑋
evth2f.4 𝑦 𝑋
evth2f.5 𝑋 = 𝐽
evth2f.6 𝐾 = ( topGen ‘ ran (,) )
evth2f.7 ( 𝜑𝐽 ∈ Comp )
evth2f.8 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
evth2f.9 ( 𝜑𝑋 ≠ ∅ )
Assertion evth2f ( 𝜑 → ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )

Proof

Step Hyp Ref Expression
1 evth2f.1 𝑥 𝐹
2 evth2f.2 𝑦 𝐹
3 evth2f.3 𝑥 𝑋
4 evth2f.4 𝑦 𝑋
5 evth2f.5 𝑋 = 𝐽
6 evth2f.6 𝐾 = ( topGen ‘ ran (,) )
7 evth2f.7 ( 𝜑𝐽 ∈ Comp )
8 evth2f.8 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
9 evth2f.9 ( 𝜑𝑋 ≠ ∅ )
10 5 6 7 8 9 evth2 ( 𝜑 → ∃ 𝑎𝑋𝑏𝑋 ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 ) )
11 nfcv 𝑎 𝑋
12 nfcv 𝑥 𝑎
13 1 12 nffv 𝑥 ( 𝐹𝑎 )
14 nfcv 𝑥
15 nfcv 𝑥 𝑏
16 1 15 nffv 𝑥 ( 𝐹𝑏 )
17 13 14 16 nfbr 𝑥 ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 )
18 3 17 nfralw 𝑥𝑏𝑋 ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 )
19 nfv 𝑎𝑏𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 )
20 fveq2 ( 𝑎 = 𝑥 → ( 𝐹𝑎 ) = ( 𝐹𝑥 ) )
21 20 breq1d ( 𝑎 = 𝑥 → ( ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 ) ↔ ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 ) ) )
22 21 ralbidv ( 𝑎 = 𝑥 → ( ∀ 𝑏𝑋 ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 ) ↔ ∀ 𝑏𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 ) ) )
23 11 3 18 19 22 cbvrexfw ( ∃ 𝑎𝑋𝑏𝑋 ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 ) ↔ ∃ 𝑥𝑋𝑏𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 ) )
24 nfcv 𝑏 𝑋
25 nfcv 𝑦 𝑥
26 2 25 nffv 𝑦 ( 𝐹𝑥 )
27 nfcv 𝑦
28 nfcv 𝑦 𝑏
29 2 28 nffv 𝑦 ( 𝐹𝑏 )
30 26 27 29 nfbr 𝑦 ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 )
31 nfv 𝑏 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 )
32 fveq2 ( 𝑏 = 𝑦 → ( 𝐹𝑏 ) = ( 𝐹𝑦 ) )
33 32 breq2d ( 𝑏 = 𝑦 → ( ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 ) ↔ ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) )
34 24 4 30 31 33 cbvralfw ( ∀ 𝑏𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 ) ↔ ∀ 𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )
35 34 rexbii ( ∃ 𝑥𝑋𝑏𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑏 ) ↔ ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )
36 23 35 bitri ( ∃ 𝑎𝑋𝑏𝑋 ( 𝐹𝑎 ) ≤ ( 𝐹𝑏 ) ↔ ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )
37 10 36 sylib ( 𝜑 → ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )