Metamath Proof Explorer

Theorem smfsuplem1

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfsuplem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smfsuplem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smfsuplem1.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfsuplem1.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smfsuplem1.d ⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
smfsuplem1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
smfsuplem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
smfsuplem1.h ⊢ ( 𝜑 → 𝐻 : 𝑍 ⟶ 𝑆 )
smfsuplem1.i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
Assertion smfsuplem1 ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step Hyp Ref Expression
1 smfsuplem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smfsuplem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smfsuplem1.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smfsuplem1.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smfsuplem1.d ⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
6 smfsuplem1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
7 smfsuplem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
8 smfsuplem1.h ⊢ ( 𝜑 → 𝐻 : 𝑍 ⟶ 𝑆 )
9 smfsuplem1.i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
11 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
12 eqid ⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 )
13 10 11 12 smff ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
14 13 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) Fn dom ( 𝐹 ‘ 𝑛 ) )
15 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝐹 ‘ 𝑛 ) Fn dom ( 𝐹 ‘ 𝑛 ) )
16 ssrab2 ⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
17 5 16 eqsstri ⊢ 𝐷 ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
18 iinss2 ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ⊆ dom ( 𝐹 ‘ 𝑛 ) )
19 17 18 sstrid ⊢ ( 𝑛 ∈ 𝑍 → 𝐷 ⊆ dom ( 𝐹 ‘ 𝑛 ) )
20 19 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝐷 ⊆ dom ( 𝐹 ‘ 𝑛 ) )
21 cnvimass ⊢ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ dom 𝐺
22 21 sseli ⊢ ( 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) → 𝑥 ∈ dom 𝐺 )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ dom 𝐺 )
24 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
25 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
26 1 25 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
27 26 2 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
28 27 ne0d ⊢ ( 𝜑 → 𝑍 ≠ ∅ )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑍 ≠ ∅ )
30 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
31 18 adantl ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ⊆ dom ( 𝐹 ‘ 𝑛 ) )
32 17 sseli ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
33 32 adantr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
34 31 33 sseldd ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
35 34 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
36 30 35 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
37 5 reqabi ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
38 37 simprbi ⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
40 24 29 36 39 suprclrnmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ )
41 40 6 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ )
42 41 fdmd ⊢ ( 𝜑 → dom 𝐺 = 𝐷 )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → dom 𝐺 = 𝐷 )
44 23 43 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ 𝐷 )
45 20 44 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
46 mnfxr ⊢ -∞ ∈ ℝ*
47 46 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → -∞ ∈ ℝ* )
48 7 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝐴 ∈ ℝ* )
50 36 an32s ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
51 44 50 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
52 51 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
53 51 mnfltd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → -∞ < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
54 22 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ dom 𝐺 )
55 41 ffdmd ⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℝ )
56 55 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
57 54 56 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
58 57 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
59 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝐴 ∈ ℝ )
60 an32 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) )
61 60 biimpi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) )
62 24 36 39 suprubrnmpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
63 61 62 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
64 6 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
65 64 40 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
66 65 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
67 63 66 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
68 44 67 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
69 46 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → -∞ ∈ ℝ* )
70 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝐴 ∈ ℝ* )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) )
72 41 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐷 )
73 elpreima ⊢ ( 𝐺 Fn 𝐷 → ( 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) ) )
74 72 73 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) ) )
76 71 75 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝑥 ∈ 𝐷 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) )
77 76 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) )
78 69 70 77 iocleubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
79 78 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
80 51 58 59 68 79 letrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 )
81 47 49 52 53 80 eliocd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) )
82 15 45 81 elpreimad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) )
83 82 ssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) )
84 inss1 ⊢ ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ⊆ ( 𝐻 ‘ 𝑛 )
85 9 84 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ⊆ ( 𝐻 ‘ 𝑛 ) )
86 83 85 sstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ( 𝐻 ‘ 𝑛 ) )
87 86 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ( 𝐻 ‘ 𝑛 ) )
88 ssiin ⊢ ( ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝑍 ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ( 𝐻 ‘ 𝑛 ) )
89 87 88 sylibr ⊢ ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) )
90 21 41 fssdm ⊢ ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ 𝐷 )
91 89 90 ssind ⊢ ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ⊆ ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
92 iniin1 ⊢ ( 𝑍 ≠ ∅ → ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) = ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
93 28 92 syl ⊢ ( 𝜑 → ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) = ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
94 72 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝐺 Fn 𝐷 )
95 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
96 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑀 ∈ 𝑍 )
97 fveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝐻 ‘ 𝑛 ) = ( 𝐻 ‘ 𝑀 ) )
98 97 ineq1d ⊢ ( 𝑛 = 𝑀 → ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) = ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) )
99 98 eleq2d ⊢ ( 𝑛 = 𝑀 → ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ↔ 𝑥 ∈ ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) ) )
100 95 96 99 eliind ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) )
101 elinel2 ⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) → 𝑥 ∈ 𝐷 )
102 100 101 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ 𝐷 )
103 46 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → -∞ ∈ ℝ* )
104 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝐴 ∈ ℝ* )
105 65 40 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
106 105 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
107 102 106 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
108 101 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) ) → 𝑥 ∈ 𝐷 )
109 108 105 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
110 109 mnfltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑀 ) ∩ 𝐷 ) ) → -∞ < ( 𝐺 ‘ 𝑥 ) )
111 100 110 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → -∞ < ( 𝐺 ‘ 𝑥 ) )
112 102 65 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
113 nfv ⊢ Ⅎ 𝑛 𝜑
114 nfcv ⊢ Ⅎ 𝑛 𝑥
115 nfii1 ⊢ Ⅎ 𝑛 ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 )
116 114 115 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 )
117 113 116 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
118 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
119 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
120 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
121 120 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
122 elinel1 ⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) → 𝑥 ∈ ( 𝐻 ‘ 𝑛 ) )
123 122 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑛 ) )
124 elinel2 ⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) → 𝑥 ∈ 𝐷 )
125 124 adantl ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ 𝐷 )
126 34 ancoms ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
127 125 126 syldan ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
128 127 3adant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
129 123 128 elind ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
130 9 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
131 129 130 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) )
132 46 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → -∞ ∈ ℝ* )
133 48 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → 𝐴 ∈ ℝ* )
134 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) )
135 elpreima ⊢ ( ( 𝐹 ‘ 𝑛 ) Fn dom ( 𝐹 ‘ 𝑛 ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) ) )
136 14 135 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) ) )
137 136 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) ) )
138 134 137 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) ) )
139 138 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) )
140 132 133 139 iocleubd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 )
141 131 140 syld3an3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 )
142 118 119 121 141 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 )
143 142 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( 𝑛 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 ) )
144 117 143 ralrimi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 )
145 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑍 ≠ ∅ )
146 102 36 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
147 102 38 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
148 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝐴 ∈ ℝ )
149 117 145 146 147 148 suprleubrnmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ≤ 𝐴 ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝐴 ) )
150 144 149 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ≤ 𝐴 )
151 112 150 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
152 103 104 107 111 151 eliocd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( -∞ (,] 𝐴 ) )
153 94 102 152 elpreimad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑥 ∈ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) )
154 153 ssd ⊢ ( 𝜑 → ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ⊆ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) )
155 93 154 eqsstrd ⊢ ( 𝜑 → ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ⊆ ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) )
156 91 155 eqssd ⊢ ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) = ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) )
157 eqid ⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
158 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
159 158 dmex ⊢ dom ( 𝐹 ‘ 𝑛 ) ∈ V
160 159 rgenw ⊢ ∀ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∈ V
161 160 a1i ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∈ V )
162 28 161 iinexd ⊢ ( 𝜑 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∈ V )
163 157 162 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ∈ V )
164 5 163 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ V )
165 2 uzct ⊢ 𝑍 ≼ ω
166 165 a1i ⊢ ( 𝜑 → 𝑍 ≼ ω )
167 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) ∈ 𝑆 )
168 3 166 28 167 saliincl ⊢ ( 𝜑 → ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∈ 𝑆 )
169 eqid ⊢ ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 )
170 3 164 168 169 elrestd ⊢ ( 𝜑 → ( ∩ 𝑛 ∈ 𝑍 ( 𝐻 ‘ 𝑛 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) )
171 156 170 eqeltrd ⊢ ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )