Proof of Theorem rnmptbd2lem
Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
2 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
3 | 2 | elrnmpt 5372 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
4 | 1, 3 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
5 | 4 | biimpi 206 |
. . . . . . . . 9
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
6 | 5 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
7 | | nfra1 2941 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 |
8 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑦 ≤ 𝑧 |
9 | | rspa 2930 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑦 ≤ 𝐵) |
10 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ≤ 𝐵 ∧ 𝑧 = 𝐵) → 𝑦 ≤ 𝐵) |
11 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝐵 → 𝑧 = 𝐵) |
12 | 11 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝐵 → 𝐵 = 𝑧) |
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ≤ 𝐵 ∧ 𝑧 = 𝐵) → 𝐵 = 𝑧) |
14 | 10, 13 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ≤ 𝐵 ∧ 𝑧 = 𝐵) → 𝑦 ≤ 𝑧) |
15 | 14 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≤ 𝐵 → (𝑧 = 𝐵 → 𝑦 ≤ 𝑧)) |
16 | 9, 15 | syl 17 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑧 = 𝐵 → 𝑦 ≤ 𝑧)) |
17 | 16 | ex 450 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑦 ≤ 𝑧))) |
18 | 7, 8, 17 | rexlimd 3026 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑦 ≤ 𝑧)) |
19 | 18 | imp 445 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑦 ≤ 𝑧) |
20 | 19 | adantll 750 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑦 ≤ 𝑧) |
21 | 6, 20 | syldan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ≤ 𝑧) |
22 | 21 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |
23 | 22 | ex 450 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) |
24 | 23 | reximdv 3016 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) |
25 | 24 | imp 445 |
. . 3
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |
26 | 25 | ex 450 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) |
27 | | rnmptbd2lem.x |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
28 | | nfmpt1 4747 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
29 | 28 | nfrn 5368 |
. . . . . . . . 9
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
30 | 29, 8 | nfral 2945 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧 |
31 | 27, 30 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |
32 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
33 | | rnmptbd2lem.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
34 | 33 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
35 | 2 | elrnmpt1 5374 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
36 | 32, 34, 35 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
37 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |
38 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → (𝑦 ≤ 𝑧 ↔ 𝑦 ≤ 𝐵)) |
39 | 38 | rspcva 3307 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) → 𝑦 ≤ 𝐵) |
40 | 36, 37, 39 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → 𝑦 ≤ 𝐵) |
41 | 40 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) → (𝑥 ∈ 𝐴 → 𝑦 ≤ 𝐵)) |
42 | 31, 41 | ralrimi 2957 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) → ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) |
43 | 42 | ex 450 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧 → ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵)) |
44 | 43 | a1d 25 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧 → ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵))) |
45 | 44 | imp 445 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧 → ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵)) |
46 | 45 | reximdva 3017 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵)) |
47 | 26, 46 | impbid 202 |
1
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) |