| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) | 
| 2 |  | sge0lefi.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | 
| 3 | 2 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 4 |  | elpwinss 45054 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) | 
| 5 | 4 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) | 
| 6 | 3, 5 | fssresd 6775 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) | 
| 7 | 1, 6 | sge0xrcl 46400 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) | 
| 8 | 7 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) | 
| 9 |  | sge0lefi.1 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 10 | 9, 2 | sge0xrcl 46400 | . . . . . 6
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) | 
| 11 | 10 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘𝐹) ∈
ℝ*) | 
| 12 |  | sge0lefi.3 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 13 | 12 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐴 ∈
ℝ*) | 
| 14 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑋 ∈ 𝑉) | 
| 15 | 14, 3 | sge0less 46407 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ≤
(Σ^‘𝐹)) | 
| 16 | 15 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ≤
(Σ^‘𝐹)) | 
| 17 |  | simplr 769 | . . . . 5
⊢ (((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘𝐹) ≤ 𝐴) | 
| 18 | 8, 11, 13, 16, 17 | xrletrd 13204 | . . . 4
⊢ (((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) | 
| 19 | 18 | ralrimiva 3146 | . . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) ≤ 𝐴) → ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) | 
| 20 | 19 | ex 412 | . 2
⊢ (𝜑 →
((Σ^‘𝐹) ≤ 𝐴 → ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴)) | 
| 21 | 9, 2 | sge0sup 46406 | . . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) | 
| 22 | 21 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) | 
| 23 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 24 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 25 | 24 | elrnmpt 5969 | . . . . . . . . . 10
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑦 =
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 26 | 23, 25 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 27 | 26 | biimpi 216 | . . . . . . . 8
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 28 | 27 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 29 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 | 
| 30 |  | nfra1 3284 | . . . . . . . . . 10
⊢
Ⅎ𝑥∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴 | 
| 31 | 29, 30 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) | 
| 32 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 | 
| 33 |  | nfmpt1 5250 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 34 | 33 | nfrn 5963 | . . . . . . . . . 10
⊢
Ⅎ𝑥ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 35 | 32, 34 | nfel 2920 | . . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 36 | 31, 35 | nfan 1899 | . . . . . . . 8
⊢
Ⅎ𝑥((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) | 
| 37 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ≤ 𝐴 | 
| 38 |  | simp3 1139 | . . . . . . . . . . . 12
⊢
((∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) → 𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) | 
| 39 |  | rspa 3248 | . . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) | 
| 40 | 39 | 3adant3 1133 | . . . . . . . . . . . 12
⊢
((∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) →
(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) | 
| 41 | 38, 40 | eqbrtrd 5165 | . . . . . . . . . . 11
⊢
((∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) → 𝑦 ≤ 𝐴) | 
| 42 | 41 | 3adant1l 1177 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 =
(Σ^‘(𝐹 ↾ 𝑥))) → 𝑦 ≤ 𝐴) | 
| 43 | 42 | 3exp 1120 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑦 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑦 ≤ 𝐴))) | 
| 44 | 43 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑦 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑦 ≤ 𝐴))) | 
| 45 | 36, 37, 44 | rexlimd 3266 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑦 =
(Σ^‘(𝐹 ↾ 𝑥)) → 𝑦 ≤ 𝐴)) | 
| 46 | 28, 45 | mpd 15 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) → 𝑦 ≤ 𝐴) | 
| 47 | 46 | ralrimiva 3146 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) → ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 ≤ 𝐴) | 
| 48 | 7 | ralrimiva 3146 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) | 
| 49 | 24 | rnmptss 7143 | . . . . . . . 8
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) | 
| 50 | 48, 49 | syl 17 | . . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) | 
| 51 | 50 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) | 
| 52 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) → 𝐴 ∈
ℝ*) | 
| 53 |  | supxrleub 13368 | . . . . . 6
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆ ℝ* ∧ 𝐴 ∈ ℝ*)
→ (sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 ≤ 𝐴)) | 
| 54 | 51, 52, 53 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))𝑦 ≤ 𝐴)) | 
| 55 | 47, 54 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) ≤ 𝐴) | 
| 56 | 22, 55 | eqbrtrd 5165 | . . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴) →
(Σ^‘𝐹) ≤ 𝐴) | 
| 57 | 56 | ex 412 | . 2
⊢ (𝜑 → (∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴 →
(Σ^‘𝐹) ≤ 𝐴)) | 
| 58 | 20, 57 | impbid 212 | 1
⊢ (𝜑 →
((Σ^‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴)) |