| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smflimsuplem2.x | . . . 4
⊢ (𝜑 → 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 2 |  | smflimsuplem2.p | . . . . . 6
⊢
Ⅎ𝑚𝜑 | 
| 3 |  | eqid 2737 | . . . . . 6
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) | 
| 4 |  | smflimsuplem2.n | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑛 ∈ 𝑍) | 
| 5 |  | smflimsuplem2.z | . . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 6 | 4, 5 | eleqtrdi 2851 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑛 ∈ (ℤ≥‘𝑀)) | 
| 7 |  | uzss 12901 | . . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑀)) | 
| 8 | 6, 7 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘𝑛) ⊆ (ℤ≥‘𝑀)) | 
| 9 | 8, 5 | sseqtrrdi 4025 | . . . . . . . . . 10
⊢ (𝜑 →
(ℤ≥‘𝑛) ⊆ 𝑍) | 
| 10 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) →
(ℤ≥‘𝑛) ⊆ 𝑍) | 
| 11 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑛)) | 
| 12 | 10, 11 | sseldd 3984 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) | 
| 13 |  | smflimsuplem2.s | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 14 | 13 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) | 
| 15 |  | smflimsuplem2.f | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 16 | 15 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) | 
| 17 |  | eqid 2737 | . . . . . . . . 9
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) | 
| 18 | 14, 16, 17 | smff 46747 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) | 
| 19 | 12, 18 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) | 
| 20 |  | iinss2 5057 | . . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑛) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ dom (𝐹‘𝑚)) | 
| 21 | 20 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ dom (𝐹‘𝑚)) | 
| 22 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 23 | 21, 22 | sseldd 3984 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑋 ∈ dom (𝐹‘𝑚)) | 
| 24 | 19, 23 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑋) ∈ ℝ) | 
| 25 |  | nfmpt1 5250 | . . . . . . . . 9
⊢
Ⅎ𝑚(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) | 
| 26 |  | nfmpt1 5250 | . . . . . . . . 9
⊢
Ⅎ𝑚(𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋)) | 
| 27 |  | eluzelz 12888 | . . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) | 
| 28 | 6, 27 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑛 ∈ ℤ) | 
| 29 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) | 
| 30 | 2, 24, 29 | fmptdf 7137 | . . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)):(ℤ≥‘𝑛)⟶ℝ) | 
| 31 | 30 | ffnd 6737 | . . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) Fn (ℤ≥‘𝑛)) | 
| 32 |  | smflimsuplem2.m | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 33 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑚(ℤ≥‘𝑀) | 
| 34 |  | fvexd 6921 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑚)‘𝑋) ∈ V) | 
| 35 | 33, 2, 34 | mptfnd 45248 | . . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋)) Fn (ℤ≥‘𝑀)) | 
| 36 | 29 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) | 
| 37 |  | fvexd 6921 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑋) ∈ V) | 
| 38 | 36, 37 | fvmpt2d 7029 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑚) = ((𝐹‘𝑚)‘𝑋)) | 
| 39 | 12, 5 | eleqtrdi 2851 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑀)) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑚 ∈
(ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋)) = (𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋)) | 
| 41 | 40 | fvmpt2 7027 | . . . . . . . . . . 11
⊢ ((𝑚 ∈
(ℤ≥‘𝑀) ∧ ((𝐹‘𝑚)‘𝑋) ∈ V) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑚) = ((𝐹‘𝑚)‘𝑋)) | 
| 42 | 39, 37, 41 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑚) = ((𝐹‘𝑚)‘𝑋)) | 
| 43 | 38, 42 | eqtr4d 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑚) = ((𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋))‘𝑚)) | 
| 44 | 2, 25, 26, 28, 31, 32, 35, 28, 43 | limsupequz 45738 | . . . . . . . 8
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋)))) | 
| 45 | 5 | eqcomi 2746 | . . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) = 𝑍 | 
| 46 | 45 | mpteq1i 5238 | . . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) | 
| 47 | 46 | fveq2i 6909 | . . . . . . . . 9
⊢ (lim
sup‘(𝑚 ∈
(ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) | 
| 48 | 47 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑀) ↦ ((𝐹‘𝑚)‘𝑋))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) | 
| 49 | 44, 48 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) | 
| 50 |  | smflimsuplem2.r | . . . . . . . 8
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) | 
| 51 | 50 | renepnfd 11312 | . . . . . . 7
⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ≠ +∞) | 
| 52 | 49, 51 | eqnetrd 3008 | . . . . . 6
⊢ (𝜑 → (lim sup‘(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) ≠ +∞) | 
| 53 | 2, 3, 24, 52 | limsupubuzmpt 45734 | . . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑚 ∈ (ℤ≥‘𝑛)((𝐹‘𝑚)‘𝑋) ≤ 𝑦) | 
| 54 |  | uzid 12893 | . . . . . . 7
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) | 
| 55 |  | ne0i 4341 | . . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (ℤ≥‘𝑛) ≠ ∅) | 
| 56 | 28, 54, 55 | 3syl 18 | . . . . . 6
⊢ (𝜑 →
(ℤ≥‘𝑛) ≠ ∅) | 
| 57 | 2, 56, 24 | supxrre3rnmpt 45440 | . . . . 5
⊢ (𝜑 → (sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, < ) ∈
ℝ ↔ ∃𝑦
∈ ℝ ∀𝑚
∈ (ℤ≥‘𝑛)((𝐹‘𝑚)‘𝑋) ≤ 𝑦)) | 
| 58 | 53, 57 | mpbird 257 | . . . 4
⊢ (𝜑 → sup(ran (𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, < ) ∈
ℝ) | 
| 59 | 1, 58 | jca 511 | . . 3
⊢ (𝜑 → (𝑋 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, < ) ∈
ℝ)) | 
| 60 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) | 
| 61 | 60 | mpteq2dv 5244 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦))) | 
| 62 | 61 | rneqd 5949 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦))) | 
| 63 | 62 | supeq1d 9486 | . . . . . . 7
⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, <
)) | 
| 64 | 63 | eleq1d 2826 | . . . . . 6
⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ ↔ sup(ran (𝑚
∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ)) | 
| 65 | 64 | cbvrabv 3447 | . . . . 5
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑦 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ} | 
| 66 | 65 | eleq2i 2833 | . . . 4
⊢ (𝑋 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ↔ 𝑋 ∈
{𝑦 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ}) | 
| 67 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑚)‘𝑦) = ((𝐹‘𝑚)‘𝑋)) | 
| 68 | 67 | mpteq2dv 5244 | . . . . . . . 8
⊢ (𝑦 = 𝑋 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) | 
| 69 | 68 | rneqd 5949 | . . . . . . 7
⊢ (𝑦 = 𝑋 → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)) = ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋))) | 
| 70 | 69 | supeq1d 9486 | . . . . . 6
⊢ (𝑦 = 𝑋 → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, <
)) | 
| 71 | 70 | eleq1d 2826 | . . . . 5
⊢ (𝑦 = 𝑋 → (sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ ↔ sup(ran (𝑚
∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, < ) ∈
ℝ)) | 
| 72 | 71 | elrab 3692 | . . . 4
⊢ (𝑋 ∈ {𝑦 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ} ↔ (𝑋 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, < ) ∈
ℝ)) | 
| 73 | 66, 72 | bitri 275 | . . 3
⊢ (𝑋 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ↔ (𝑋 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑋)), ℝ*, < ) ∈
ℝ)) | 
| 74 | 59, 73 | sylibr 234 | . 2
⊢ (𝜑 → 𝑋 ∈ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 75 |  | id 22 | . . . . 5
⊢ (𝜑 → 𝜑) | 
| 76 |  | smflimsuplem2.h | . . . . . . 7
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 77 | 76 | a1i 11 | . . . . . 6
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)))) | 
| 78 |  | smflimsuplem2.e | . . . . . . . . . 10
⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 79 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑥𝑍 | 
| 80 |  | nfrab1 3457 | . . . . . . . . . . 11
⊢
Ⅎ𝑥{𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} | 
| 81 | 79, 80 | nfmpt 5249 | . . . . . . . . . 10
⊢
Ⅎ𝑥(𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 82 | 78, 81 | nfcxfr 2903 | . . . . . . . . 9
⊢
Ⅎ𝑥𝐸 | 
| 83 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑥𝑛 | 
| 84 | 82, 83 | nffv 6916 | . . . . . . . 8
⊢
Ⅎ𝑥(𝐸‘𝑛) | 
| 85 |  | fvex 6919 | . . . . . . . 8
⊢ (𝐸‘𝑛) ∈ V | 
| 86 | 84, 85 | mptexf 45243 | . . . . . . 7
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V | 
| 87 | 86 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V) | 
| 88 | 77, 87 | fvmpt2d 7029 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 89 | 75, 4, 88 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 90 | 89 | dmeqd 5916 | . . 3
⊢ (𝜑 → dom (𝐻‘𝑛) = dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 91 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑦(𝐸‘𝑛) | 
| 92 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑦sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
) | 
| 93 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑥sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, <
) | 
| 94 | 84, 91, 92, 93, 63 | cbvmptf 5251 | . . . 4
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝑦 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, <
)) | 
| 95 |  | xrltso 13183 | . . . . . 6
⊢  < Or
ℝ* | 
| 96 | 95 | supex 9503 | . . . . 5
⊢ sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
V | 
| 97 | 96 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
V) | 
| 98 | 94, 97 | dmmptd 6713 | . . 3
⊢ (𝜑 → dom (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝐸‘𝑛)) | 
| 99 |  | eqid 2737 | . . . . 5
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} | 
| 100 |  | fvex 6919 | . . . . . . . . 9
⊢ (𝐹‘𝑚) ∈ V | 
| 101 | 100 | dmex 7931 | . . . . . . . 8
⊢ dom
(𝐹‘𝑚) ∈ V | 
| 102 | 101 | rgenw 3065 | . . . . . . 7
⊢
∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V | 
| 103 | 102 | a1i 11 | . . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) | 
| 104 | 56, 103 | iinexd 45138 | . . . . 5
⊢ (𝜑 → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) | 
| 105 | 99, 104 | rabexd 5340 | . . . 4
⊢ (𝜑 → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) | 
| 106 | 78 | fvmpt2 7027 | . . . 4
⊢ ((𝑛 ∈ 𝑍 ∧ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 107 | 4, 105, 106 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 108 | 90, 98, 107 | 3eqtrrd 2782 | . 2
⊢ (𝜑 → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = dom (𝐻‘𝑛)) | 
| 109 | 74, 108 | eleqtrd 2843 | 1
⊢ (𝜑 → 𝑋 ∈ dom (𝐻‘𝑛)) |