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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )