| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smfinflem.g | . . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) | 
| 2 | 1 | a1i 11 | . . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))) | 
| 3 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐷) | 
| 4 |  | smfinflem.m | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 5 |  | smfinflem.z | . . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 6 | 4, 5 | uzn0d 45441 | . . . . . 6
⊢ (𝜑 → 𝑍 ≠ ∅) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑍 ≠ ∅) | 
| 8 |  | smfinflem.s | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 9 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) | 
| 10 |  | smfinflem.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 11 | 10 | ffvelcdmda 7103 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (SMblFn‘𝑆)) | 
| 12 |  | eqid 2736 | . . . . . . . 8
⊢ dom
(𝐹‘𝑛) = dom (𝐹‘𝑛) | 
| 13 | 9, 11, 12 | smff 46752 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ) | 
| 14 | 13 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ) | 
| 15 |  | ssrab2 4079 | . . . . . . . . . 10
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} ⊆ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) | 
| 16 |  | smfinflem.d | . . . . . . . . . . . 12
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} | 
| 17 | 16 | eleq2i 2832 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}) | 
| 18 | 17 | biimpi 216 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}) | 
| 19 | 15, 18 | sselid 3980 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) | 
| 21 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) | 
| 22 |  | eliinid 45121 | . . . . . . . 8
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) | 
| 23 | 20, 21, 22 | syl2anc 584 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) | 
| 24 | 23 | adantll 714 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) | 
| 25 | 14, 24 | ffvelcdmd 7104 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 26 |  | rabidim2 45112 | . . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 27 | 18, 26 | syl 17 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 28 | 27 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 29 | 3, 7, 25, 28 | infnsuprnmpt 45262 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = -sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) | 
| 30 | 29 | mpteq2dva 5241 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ 𝐷 ↦ -sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ))) | 
| 31 | 2, 30 | eqtrd 2776 | . 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ -sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ))) | 
| 32 |  | nfv 1913 | . . 3
⊢
Ⅎ𝑥𝜑 | 
| 33 |  | fvex 6918 | . . . . . . . 8
⊢ (𝐹‘𝑛) ∈ V | 
| 34 | 33 | dmex 7932 | . . . . . . 7
⊢ dom
(𝐹‘𝑛) ∈ V | 
| 35 | 34 | rgenw 3064 | . . . . . 6
⊢
∀𝑛 ∈
𝑍 dom (𝐹‘𝑛) ∈ V | 
| 36 | 35 | a1i 11 | . . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∈ V) | 
| 37 | 6, 36 | iinexd 45143 | . . . 4
⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∈ V) | 
| 38 | 16, 37 | rabexd 5339 | . . 3
⊢ (𝜑 → 𝐷 ∈ V) | 
| 39 | 25 | renegcld 11691 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → -((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 40 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → ((𝐹‘𝑚)‘𝑤) = ((𝐹‘𝑚)‘𝑥)) | 
| 41 | 40 | breq2d 5154 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑧 ≤ ((𝐹‘𝑚)‘𝑤) ↔ 𝑧 ≤ ((𝐹‘𝑚)‘𝑥))) | 
| 42 | 41 | ralbidv 3177 | . . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤) ↔ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥))) | 
| 43 | 42 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤) ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥))) | 
| 44 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑤∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) | 
| 45 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑍 | 
| 46 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝐹‘𝑚) | 
| 47 | 46 | nfdm 5961 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥dom
(𝐹‘𝑚) | 
| 48 | 45, 47 | nfiin 5023 | . . . . . . . . . . 11
⊢
Ⅎ𝑥∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚) | 
| 49 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑤∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) | 
| 50 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤) | 
| 51 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑚dom
(𝐹‘𝑛) | 
| 52 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝐹‘𝑚) | 
| 53 | 52 | nfdm 5961 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛dom
(𝐹‘𝑚) | 
| 54 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) | 
| 55 | 54 | dmeqd 5915 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → dom (𝐹‘𝑛) = dom (𝐹‘𝑚)) | 
| 56 | 51, 53, 55 | cbviin 5036 | . . . . . . . . . . . 12
⊢ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) = ∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚) | 
| 57 | 56 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) = ∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚)) | 
| 58 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑤)) | 
| 59 | 58 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ 𝑦 ≤ ((𝐹‘𝑛)‘𝑤))) | 
| 60 | 59 | ralbidv 3177 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑤))) | 
| 61 |  | nfv 1913 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚 𝑦 ≤ ((𝐹‘𝑛)‘𝑤) | 
| 62 |  | nfcv 2904 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛𝑦 | 
| 63 |  | nfcv 2904 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛
≤ | 
| 64 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛𝑤 | 
| 65 | 52, 64 | nffv 6915 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛((𝐹‘𝑚)‘𝑤) | 
| 66 | 62, 63, 65 | nfbr 5189 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛 𝑦 ≤ ((𝐹‘𝑚)‘𝑤) | 
| 67 | 54 | fveq1d 6907 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑤) = ((𝐹‘𝑚)‘𝑤)) | 
| 68 | 67 | breq2d 5154 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑦 ≤ ((𝐹‘𝑛)‘𝑤) ↔ 𝑦 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 69 | 61, 66, 68 | cbvralw 3305 | . . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑤) ↔ ∀𝑚 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤)) | 
| 70 | 69 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑤) ↔ ∀𝑚 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 71 | 60, 70 | bitrd 279 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑚 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 72 | 71 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 73 |  | breq1 5145 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑦 ≤ ((𝐹‘𝑚)‘𝑤) ↔ 𝑧 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 74 | 73 | ralbidv 3177 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (∀𝑚 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤) ↔ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 75 | 74 | cbvrexvw 3237 | . . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
ℝ ∀𝑚 ∈
𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤) ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤)) | 
| 76 | 75 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑚)‘𝑤) ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 77 | 72, 76 | bitrd 279 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤))) | 
| 78 | 44, 48, 49, 50, 57, 77 | cbvrabcsfw 3939 | . . . . . . . . . 10
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑤 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∣ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤)} | 
| 79 | 16, 78 | eqtri 2764 | . . . . . . . . 9
⊢ 𝐷 = {𝑤 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∣ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑤)} | 
| 80 | 43, 79 | elrab2 3694 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∧ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥))) | 
| 81 | 80 | biimpi 216 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝑥 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∧ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥))) | 
| 82 | 81 | simprd 495 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) | 
| 83 | 82 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) | 
| 84 |  | renegcl 11573 | . . . . . . . 8
⊢ (𝑧 ∈ ℝ → -𝑧 ∈
ℝ) | 
| 85 | 84 | ad2antlr 727 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) → -𝑧 ∈ ℝ) | 
| 86 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) | 
| 87 | 86 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑛)‘𝑥)) | 
| 88 | 87 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑧 ≤ ((𝐹‘𝑚)‘𝑥) ↔ 𝑧 ≤ ((𝐹‘𝑛)‘𝑥))) | 
| 89 | 88 | rspcva 3619 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) → 𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 90 | 89 | ancoms 458 | . . . . . . . . . 10
⊢
((∀𝑚 ∈
𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥) ∧ 𝑛 ∈ 𝑍) → 𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 91 | 90 | adantll 714 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 92 |  | simpllr 775 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑧 ∈ ℝ) | 
| 93 | 25 | ad4ant14 752 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 94 | 92, 93 | lenegd 11843 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → (𝑧 ≤ ((𝐹‘𝑛)‘𝑥) ↔ -((𝐹‘𝑛)‘𝑥) ≤ -𝑧)) | 
| 95 | 91, 94 | mpbid 232 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → -((𝐹‘𝑛)‘𝑥) ≤ -𝑧) | 
| 96 | 95 | ralrimiva 3145 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) → ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ -𝑧) | 
| 97 |  | brralrspcev 5202 | . . . . . . 7
⊢ ((-𝑧 ∈ ℝ ∧
∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ -𝑧) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑦) | 
| 98 | 85, 96, 97 | syl2anc 584 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑦) | 
| 99 | 98 | rexlimdva2 3156 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 𝑧 ≤ ((𝐹‘𝑚)‘𝑥) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑦)) | 
| 100 | 83, 99 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑦) | 
| 101 | 3, 7, 39, 100 | suprclrnmpt 45263 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) | 
| 102 | 16 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}) | 
| 103 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) | 
| 104 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑦∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧 | 
| 105 |  | renegcl 11573 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) | 
| 106 | 105 | 3ad2ant2 1134 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → -𝑦 ∈ ℝ) | 
| 107 |  | nfv 1913 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝜑 | 
| 108 |  | nfcv 2904 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛𝑥 | 
| 109 |  | nfii1 5028 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) | 
| 110 | 108, 109 | nfel 2919 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) | 
| 111 | 107, 110 | nfan 1898 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) | 
| 112 | 62 | nfel1 2921 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑦 ∈ ℝ | 
| 113 |  | nfra1 3283 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) | 
| 114 | 111, 112,
113 | nf3an 1900 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 115 |  | simpl2 1192 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑦 ∈ ℝ) | 
| 116 |  | simpll 766 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝜑) | 
| 117 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) | 
| 118 | 22 | adantll 714 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) | 
| 119 | 13 | 3adant3 1132 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ) | 
| 120 |  | simp3 1138 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → 𝑥 ∈ dom (𝐹‘𝑛)) | 
| 121 | 119, 120 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 122 | 116, 117,
118, 121 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 123 | 122 | 3ad2antl1 1185 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 124 |  | rspa 3247 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ∧ 𝑛 ∈ 𝑍) → 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 125 | 124 | 3ad2antl3 1187 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 126 |  | leneg 11767 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ ∧ ((𝐹‘𝑛)‘𝑥) ∈ ℝ) → (𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ -((𝐹‘𝑛)‘𝑥) ≤ -𝑦)) | 
| 127 | 126 | biimp3a 1470 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ ((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → -((𝐹‘𝑛)‘𝑥) ≤ -𝑦) | 
| 128 | 115, 123,
125, 127 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) ∧ 𝑛 ∈ 𝑍) → -((𝐹‘𝑛)‘𝑥) ≤ -𝑦) | 
| 129 | 128 | ex 412 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → (𝑛 ∈ 𝑍 → -((𝐹‘𝑛)‘𝑥) ≤ -𝑦)) | 
| 130 | 114, 129 | ralrimi 3256 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ -𝑦) | 
| 131 |  | brralrspcev 5202 | . . . . . . . . . . . 12
⊢ ((-𝑦 ∈ ℝ ∧
∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ -𝑦) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) | 
| 132 | 106, 130,
131 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) | 
| 133 | 132 | 3exp 1119 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (𝑦 ∈ ℝ → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧))) | 
| 134 | 103, 104,
133 | rexlimd 3265 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧)) | 
| 135 | 84 | 3ad2ant2 1134 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → -𝑧 ∈ ℝ) | 
| 136 |  | nfv 1913 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑧 ∈ ℝ | 
| 137 |  | nfra1 3283 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧 | 
| 138 | 111, 136,
137 | nf3an 1900 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) | 
| 139 | 122 | 3ad2antl1 1185 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 140 |  | simpl2 1192 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛 ∈ 𝑍) → 𝑧 ∈ ℝ) | 
| 141 |  | rspa 3247 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧 ∧ 𝑛 ∈ 𝑍) → -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) | 
| 142 | 141 | 3ad2antl3 1187 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛 ∈ 𝑍) → -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) | 
| 143 |  | simp3 1138 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) | 
| 144 |  | renegcl 11573 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝑛)‘𝑥) ∈ ℝ → -((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 145 | 144 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → -((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 146 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ) | 
| 147 |  | leneg 11767 | . . . . . . . . . . . . . . . . . . 19
⊢
((-((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-((𝐹‘𝑛)‘𝑥) ≤ 𝑧 ↔ -𝑧 ≤ --((𝐹‘𝑛)‘𝑥))) | 
| 148 | 145, 146,
147 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-((𝐹‘𝑛)‘𝑥) ≤ 𝑧 ↔ -𝑧 ≤ --((𝐹‘𝑛)‘𝑥))) | 
| 149 | 148 | 3adant3 1132 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → (-((𝐹‘𝑛)‘𝑥) ≤ 𝑧 ↔ -𝑧 ≤ --((𝐹‘𝑛)‘𝑥))) | 
| 150 | 143, 149 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → -𝑧 ≤ --((𝐹‘𝑛)‘𝑥)) | 
| 151 |  | recn 11246 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑛)‘𝑥) ∈ ℝ → ((𝐹‘𝑛)‘𝑥) ∈ ℂ) | 
| 152 | 151 | negnegd 11612 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑛)‘𝑥) ∈ ℝ → --((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥)) | 
| 153 | 152 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → --((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥)) | 
| 154 | 150, 153 | breqtrd 5168 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → -𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 155 | 139, 140,
142, 154 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛 ∈ 𝑍) → -𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 156 | 155 | ex 412 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → (𝑛 ∈ 𝑍 → -𝑧 ≤ ((𝐹‘𝑛)‘𝑥))) | 
| 157 | 138, 156 | ralrimi 3256 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → ∀𝑛 ∈ 𝑍 -𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 158 |  | breq1 5145 | . . . . . . . . . . . . . 14
⊢ (𝑦 = -𝑧 → (𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ -𝑧 ≤ ((𝐹‘𝑛)‘𝑥))) | 
| 159 | 158 | ralbidv 3177 | . . . . . . . . . . . . 13
⊢ (𝑦 = -𝑧 → (∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∀𝑛 ∈ 𝑍 -𝑧 ≤ ((𝐹‘𝑛)‘𝑥))) | 
| 160 | 159 | rspcev 3621 | . . . . . . . . . . . 12
⊢ ((-𝑧 ∈ ℝ ∧
∀𝑛 ∈ 𝑍 -𝑧 ≤ ((𝐹‘𝑛)‘𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 161 | 135, 157,
160 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)) | 
| 162 | 161 | 3exp 1119 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (𝑧 ∈ ℝ → (∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧 → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)))) | 
| 163 | 162 | rexlimdv 3152 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧 → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥))) | 
| 164 | 134, 163 | impbid 212 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥) ↔ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧)) | 
| 165 | 32, 164 | rabbida 3462 | . . . . . . 7
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧}) | 
| 166 | 102, 165 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧}) | 
| 167 | 32, 166 | alrimi 2212 | . . . . 5
⊢ (𝜑 → ∀𝑥 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧}) | 
| 168 |  | eqid 2736 | . . . . . . 7
⊢ sup(ran
(𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) | 
| 169 | 168 | rgenw 3064 | . . . . . 6
⊢
∀𝑥 ∈
𝐷 sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) | 
| 170 | 169 | a1i 11 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐷 sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) | 
| 171 |  | mpteq12f 5229 | . . . . 5
⊢
((∀𝑥 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} ∧ ∀𝑥 ∈ 𝐷 sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) → (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ))) | 
| 172 | 167, 170,
171 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < ))) | 
| 173 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑧𝜑 | 
| 174 | 121 | renegcld 11691 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → -((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 175 |  | nfv 1913 | . . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍) | 
| 176 | 34 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ V) | 
| 177 | 121 | 3expa 1118 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑛)) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) | 
| 178 | 13 | feqmptd 6976 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = (𝑥 ∈ dom (𝐹‘𝑛) ↦ ((𝐹‘𝑛)‘𝑥))) | 
| 179 | 178 | eqcomd 2742 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ dom (𝐹‘𝑛) ↦ ((𝐹‘𝑛)‘𝑥)) = (𝐹‘𝑛)) | 
| 180 | 179, 11 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ dom (𝐹‘𝑛) ↦ ((𝐹‘𝑛)‘𝑥)) ∈ (SMblFn‘𝑆)) | 
| 181 | 175, 9, 176, 177, 180 | smfneg 46823 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ dom (𝐹‘𝑛) ↦ -((𝐹‘𝑛)‘𝑥)) ∈ (SMblFn‘𝑆)) | 
| 182 |  | eqid 2736 | . . . . 5
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} | 
| 183 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) | 
| 184 | 107, 32, 173, 4, 5, 8, 174, 181, 182, 183 | smfsupmpt 46835 | . . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛 ∈ 𝑍 -((𝐹‘𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) ∈
(SMblFn‘𝑆)) | 
| 185 | 172, 184 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) ∈
(SMblFn‘𝑆)) | 
| 186 | 32, 8, 38, 101, 185 | smfneg 46823 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ -sup(ran (𝑛 ∈ 𝑍 ↦ -((𝐹‘𝑛)‘𝑥)), ℝ, < )) ∈
(SMblFn‘𝑆)) | 
| 187 | 31, 186 | eqeltrd 2840 | 1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |