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

Proof

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