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 ∧ ∀ 𝑦𝐴 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝐵𝑥 )