| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sge0pnffigt.y | . . 3
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 2 |  | sge0pnffigt.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 3 |  | sge0pnffigt.f | . . . . . 6
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | 
| 4 | 2, 3 | sge0sup 46406 | . . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) | 
| 5 |  | sge0pnffigt.pnf | . . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) = +∞) | 
| 6 | 4, 5 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) | 
| 7 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 8 | 7 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ V) | 
| 9 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 10 |  | elpwinss 45054 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) | 
| 11 | 10 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) | 
| 12 | 9, 11 | fssresd 6775 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) | 
| 13 | 8, 12 | sge0xrcl 46400 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) | 
| 14 | 13 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) | 
| 15 |  | eqid 2737 | . . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 16 | 15 | rnmptss 7143 | . . . . . 6
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) | 
| 17 | 14, 16 | syl 17 | . . . . 5
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) | 
| 18 |  | supxrunb2 13362 | . . . . 5
⊢ (ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆ ℝ* →
(∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 < 𝑧 ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞)) | 
| 19 | 17, 18 | syl 17 | . . . 4
⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 < 𝑧 ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞)) | 
| 20 | 6, 19 | mpbird 257 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ ℝ ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 < 𝑧) | 
| 21 |  | breq1 5146 | . . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 < 𝑧 ↔ 𝑌 < 𝑧)) | 
| 22 | 21 | rexbidv 3179 | . . . 4
⊢ (𝑦 = 𝑌 → (∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 < 𝑧 ↔ ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑌 < 𝑧)) | 
| 23 | 22 | rspcva 3620 | . . 3
⊢ ((𝑌 ∈ ℝ ∧
∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 < 𝑧) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑌 < 𝑧) | 
| 24 | 1, 20, 23 | syl2anc 584 | . 2
⊢ (𝜑 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑌 < 𝑧) | 
| 25 |  | vex 3484 | . . . . . . . 8
⊢ 𝑧 ∈ V | 
| 26 | 15 | elrnmpt 5969 | . . . . . . . 8
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑧 =
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 27 | 25, 26 | ax-mp 5 | . . . . . . 7
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 28 | 27 | biimpi 216 | . . . . . 6
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 29 | 28 | 3ad2ant2 1135 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ∧ 𝑌 < 𝑧) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 30 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑥𝜑 | 
| 31 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑥𝑧 | 
| 32 |  | nfmpt1 5250 | . . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 33 | 32 | nfrn 5963 | . . . . . . . 8
⊢
Ⅎ𝑥ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 34 | 31, 33 | nfel 2920 | . . . . . . 7
⊢
Ⅎ𝑥 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 35 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑥 𝑌 < 𝑧 | 
| 36 | 30, 34, 35 | nf3an 1901 | . . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ∧ 𝑌 < 𝑧) | 
| 37 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑌 < 𝑧 ∧ 𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) → 𝑌 < 𝑧) | 
| 38 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑌 < 𝑧 ∧ 𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) → 𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 39 | 38 | breq2d 5155 | . . . . . . . . . . 11
⊢ ((𝑌 < 𝑧 ∧ 𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) → (𝑌 < 𝑧 ↔ 𝑌 <
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 40 | 37, 39 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝑌 < 𝑧 ∧ 𝑧 =
(Σ^‘(𝐹 ↾ 𝑥))) → 𝑌 <
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 41 | 40 | ex 412 | . . . . . . . . 9
⊢ (𝑌 < 𝑧 → (𝑧 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑌 <
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 42 | 41 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 < 𝑧) → (𝑧 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑌 <
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 43 | 42 | a1d 25 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑌 < 𝑧) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑧 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑌 <
(Σ^‘(𝐹 ↾ 𝑥))))) | 
| 44 | 43 | 3adant2 1132 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ∧ 𝑌 < 𝑧) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑧 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑌 <
(Σ^‘(𝐹 ↾ 𝑥))))) | 
| 45 | 36, 44 | reximdai 3261 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ∧ 𝑌 < 𝑧) → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑧 =
(Σ^‘(𝐹 ↾ 𝑥)) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑌 <
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 46 | 29, 45 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ∧ 𝑌 < 𝑧) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑌 <
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 47 | 46 | 3exp 1120 | . . 3
⊢ (𝜑 → (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) → (𝑌 < 𝑧 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑌 <
(Σ^‘(𝐹 ↾ 𝑥))))) | 
| 48 | 47 | rexlimdv 3153 | . 2
⊢ (𝜑 → (∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑌 < 𝑧 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑌 <
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 49 | 24, 48 | mpd 15 | 1
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑌 <
(Σ^‘(𝐹 ↾ 𝑥))) |