Metamath Proof Explorer

Theorem fimaxre3

Description: A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014)

Ref Expression
Assertion fimaxre3 ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ ∧ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 ∈ ℝ ∧ 𝑧 = 𝐵 ) )
2 eleq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
3 2 biimparc ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑧 = 𝐵 ) → 𝑧 ∈ ℝ )
4 3 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝐵 ∈ ℝ ∧ 𝑧 = 𝐵 ) → 𝑧 ∈ ℝ )
5 1 4 syl ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ ∧ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑧 ∈ ℝ )
6 5 ex ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ → ( ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ∈ ℝ ) )
7 6 abssdv ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ → { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ )
8 abrexfi ⊢ ( 𝐴 ∈ Fin → { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } ∈ Fin )
9 fimaxre2 ⊢ ( ( { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ ∧ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 )
10 7 8 9 syl2anr ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 )
11 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) )
12 11 albii ⊢ ( ∀ 𝑤 ∀ 𝑦 ∈ 𝐴 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ ∀ 𝑤 ( ∃ 𝑦 ∈ 𝐴 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) )
13 ralcom4 ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ ∀ 𝑤 ∀ 𝑦 ∈ 𝐴 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) )
14 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = 𝐵 ↔ 𝑤 = 𝐵 ) )
15 14 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑤 = 𝐵 ) )
16 15 ralab ⊢ ( ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 ↔ ∀ 𝑤 ( ∃ 𝑦 ∈ 𝐴 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) )
17 12 13 16 3bitr4i ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 )
18 nfv ⊢ Ⅎ 𝑤 𝐵 ≤ 𝑥
19 breq1 ⊢ ( 𝑤 = 𝐵 → ( 𝑤 ≤ 𝑥 ↔ 𝐵 ≤ 𝑥 ) )
20 18 19 ceqsalg ⊢ ( 𝐵 ∈ ℝ → ( ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ 𝐵 ≤ 𝑥 ) )
21 20 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ → ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ 𝐵 ≤ 𝑥 ) )
22 ralbi ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ 𝐵 ≤ 𝑥 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 ) )
23 21 22 syl ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑤 ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 ) )
24 17 23 bitr3id ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ → ( ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 ) )
25 24 rexbidv ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 ) )
26 25 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 ) )
27 10 26 mpbid ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝐵 ≤ 𝑥 )