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