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 ⊢ A ∈ Fin ∧ ∀ y ∈ A B ∈ ℝ → ∃ x ∈ ℝ ∀ y ∈ A B ≤ x

Proof

Step Hyp Ref Expression
1 r19.29 ⊢ ∀ y ∈ A B ∈ ℝ ∧ ∃ y ∈ A z = B → ∃ y ∈ A B ∈ ℝ ∧ z = B
2 eleq1 ⊢ z = B → z ∈ ℝ ↔ B ∈ ℝ
3 2 biimparc ⊢ B ∈ ℝ ∧ z = B → z ∈ ℝ
4 3 rexlimivw ⊢ ∃ y ∈ A B ∈ ℝ ∧ z = B → z ∈ ℝ
5 1 4 syl ⊢ ∀ y ∈ A B ∈ ℝ ∧ ∃ y ∈ A z = B → z ∈ ℝ
6 5 ex ⊢ ∀ y ∈ A B ∈ ℝ → ∃ y ∈ A z = B → z ∈ ℝ
7 6 abssdv ⊢ ∀ y ∈ A B ∈ ℝ → z | ∃ y ∈ A z = B ⊆ ℝ
8 abrexfi ⊢ A ∈ Fin → z | ∃ y ∈ A z = B ∈ Fin
9 fimaxre2 ⊢ z | ∃ y ∈ A z = B ⊆ ℝ ∧ z | ∃ y ∈ A z = B ∈ Fin → ∃ x ∈ ℝ ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x
10 7 8 9 syl2anr ⊢ A ∈ Fin ∧ ∀ y ∈ A B ∈ ℝ → ∃ x ∈ ℝ ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x
11 r19.23v ⊢ ∀ y ∈ A w = B → w ≤ x ↔ ∃ y ∈ A w = B → w ≤ x
12 11 albii ⊢ ∀ w ∀ y ∈ A w = B → w ≤ x ↔ ∀ w ∃ y ∈ A w = B → w ≤ x
13 ralcom4 ⊢ ∀ y ∈ A ∀ w w = B → w ≤ x ↔ ∀ w ∀ y ∈ A w = B → w ≤ x
14 eqeq1 ⊢ z = w → z = B ↔ w = B
15 14 rexbidv ⊢ z = w → ∃ y ∈ A z = B ↔ ∃ y ∈ A w = B
16 15 ralab ⊢ ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x ↔ ∀ w ∃ y ∈ A w = B → w ≤ x
17 12 13 16 3bitr4i ⊢ ∀ y ∈ A ∀ w w = B → w ≤ x ↔ ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x
18 nfv ⊢ Ⅎ w B ≤ x
19 breq1 ⊢ w = B → w ≤ x ↔ B ≤ x
20 18 19 ceqsalg ⊢ B ∈ ℝ → ∀ w w = B → w ≤ x ↔ B ≤ x
21 20 ralimi ⊢ ∀ y ∈ A B ∈ ℝ → ∀ y ∈ A ∀ w w = B → w ≤ x ↔ B ≤ x
22 ralbi ⊢ ∀ y ∈ A ∀ w w = B → w ≤ x ↔ B ≤ x → ∀ y ∈ A ∀ w w = B → w ≤ x ↔ ∀ y ∈ A B ≤ x
23 21 22 syl ⊢ ∀ y ∈ A B ∈ ℝ → ∀ y ∈ A ∀ w w = B → w ≤ x ↔ ∀ y ∈ A B ≤ x
24 17 23 bitr3id ⊢ ∀ y ∈ A B ∈ ℝ → ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x ↔ ∀ y ∈ A B ≤ x
25 24 rexbidv ⊢ ∀ y ∈ A B ∈ ℝ → ∃ x ∈ ℝ ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x ↔ ∃ x ∈ ℝ ∀ y ∈ A B ≤ x
26 25 adantl ⊢ A ∈ Fin ∧ ∀ y ∈ A B ∈ ℝ → ∃ x ∈ ℝ ∀ w ∈ z | ∃ y ∈ A z = B w ≤ x ↔ ∃ x ∈ ℝ ∀ y ∈ A B ≤ x
27 10 26 mpbid ⊢ A ∈ Fin ∧ ∀ y ∈ A B ∈ ℝ → ∃ x ∈ ℝ ∀ y ∈ A B ≤ x