Metamath Proof Explorer

Theorem smflimlem2

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflimlem2.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimlem2.2 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimlem2.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflimlem2.4 ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
smflimlem2.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
smflimlem2.6 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
smflimlem2.7 ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
smflimlem2.8 ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
smflimlem2.9 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
smflimlem2.10 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
Assertion smflimlem2 ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷 ∩ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 smflimlem2.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 smflimlem2.2 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3 smflimlem2.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
4 smflimlem2.4 ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
5 smflimlem2.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
6 smflimlem2.6 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7 smflimlem2.7 ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
8 smflimlem2.8 ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
9 smflimlem2.9 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
10 smflimlem2.10 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
11 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
12 4 11 nfcxfr ⊢ Ⅎ 𝑥 𝐷
13 12 ssrab2f ⊢ { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐷
14 13 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐷 )
15 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ 𝐷 )
16 ssrab2 ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
17 4 16 eqsstri ⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
18 17 sseli ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
19 fveq2 ⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) )
20 19 iineq1d ⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
21 20 cbviunv ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
22 21 eleq2i ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
23 eliun ⊢ ( 𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
24 22 23 bitri ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
25 18 24 sylib ⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
26 15 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
27 nfv ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
28 nfv ⊢ Ⅎ 𝑚 𝑘 ∈ ℕ
29 27 28 nfan ⊢ Ⅎ 𝑚 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ )
30 nfv ⊢ Ⅎ 𝑚 𝑖 ∈ 𝑍
31 29 30 nfan ⊢ Ⅎ 𝑚 ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 )
32 nfcv ⊢ Ⅎ 𝑚 𝑥
33 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
34 32 33 nfel ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
35 31 34 nfan ⊢ Ⅎ 𝑚 ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
36 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
37 eqid ⊢ ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑖 )
38 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
39 1 eleq2i ⊢ ( 𝑖 ∈ 𝑍 ↔ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
40 39 biimpi ⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
41 38 40 sselid ⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ℤ )
42 uzid ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) )
43 41 42 syl ⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) )
44 43 ad2antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) )
45 simplll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) )
46 45 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 )
47 uzss ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
48 40 47 syl ⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
49 48 1 sseqtrrdi ⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 )
50 49 sselda ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑚 ∈ 𝑍 )
51 50 ad4ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑚 ∈ 𝑍 )
52 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
53 52 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
54 eqidd ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
55 fvexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
56 54 55 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
57 56 3adant3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
58 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
59 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
60 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
61 58 59 60 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
62 61 3adant3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
63 simp3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
64 62 63 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
65 57 64 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
66 46 51 53 65 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
67 66 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
68 67 adantl3r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
69 4 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
70 69 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
71 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
72 70 71 syl ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
73 climdm ⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
74 72 73 sylib ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
76 75 73 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
77 76 73 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
78 nfcv ⊢ Ⅎ 𝑥 𝐹
79 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
80 12 78 5 79 fnlimfv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
81 80 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝑥 ) )
82 77 81 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
83 82 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
84 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝐴 ∈ ℝ )
85 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
86 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
87 nnrecrp ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
88 86 87 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 1 / 𝑘 ) ∈ ℝ+ )
89 35 36 37 44 68 83 84 85 88 climleltrp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
90 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 )
91 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑖 ∈ 𝑍 )
92 91 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑖 ∈ 𝑍 )
93 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
94 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) )
95 nfv ⊢ Ⅎ 𝑚 𝜑
96 95 30 34 nf3an ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
97 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ ( ℤ≥ ‘ 𝑖 )
98 96 97 nfan ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) )
99 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) )
100 37 uztrn2 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) )
101 100 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) )
102 simpll2 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑖 ∈ 𝑍 )
103 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) )
104 102 103 50 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑚 ∈ 𝑍 )
105 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
106 id ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍 )
107 fvexd ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
108 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
109 108 fvmpt2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
110 106 107 109 syl2anc ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
111 110 eqcomd ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) )
112 111 adantr ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) )
113 simpr ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
114 112 113 eqbrtrd ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
115 104 105 114 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
116 52 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
118 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
119 117 118 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
120 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
121 119 120 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
122 115 121 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
123 122 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
124 123 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
125 99 101 124 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
126 98 125 ralimdaa ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
127 90 92 93 94 126 syl31anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
128 127 reximdva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
129 89 128 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
130 ssrexv ⊢ ( ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
131 49 130 syl ⊢ ( 𝑖 ∈ 𝑍 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
132 131 ad2antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
133 129 132 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
134 133 rexlimdva2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
135 26 134 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
136 nfv ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 )
137 nfra1 ⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) }
138 136 137 nfan ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
139 simpll1 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
140 simpll2 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
141 1 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 )
142 141 ssd ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
143 142 sselda ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
144 143 adantll ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
145 144 3adantl1 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
146 145 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
147 rspa ⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
148 147 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
149 simp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝜑 )
150 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
151 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑘 ∈ ℕ )
152 eqid ⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
153 152 2 rabexd ⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
154 153 ralrimivw ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
155 154 ralrimivw ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
156 155 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
157 7 elrnmpoid ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 )
158 150 151 156 157 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 )
159 ovex ⊢ ( 𝑚 𝑃 𝑘 ) ∈ V
160 eleq1 ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝑟 ∈ ran 𝑃 ↔ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) )
161 160 anbi2d ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) ↔ ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) ) )
162 fveq2 ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝐶 ‘ 𝑟 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
163 id ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → 𝑟 = ( 𝑚 𝑃 𝑘 ) )
164 162 163 eleq12d ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ↔ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) )
165 161 164 imbi12d ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) ↔ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) ) )
166 159 165 10 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) )
167 149 158 166 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) )
168 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V )
169 8 ovmpt4g ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
170 150 151 168 169 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
171 170 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝑚 𝐻 𝑘 ) )
172 149 153 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
173 7 ovmpt4g ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
174 150 151 172 173 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
175 171 174 eleq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ↔ ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
176 167 175 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
177 ineq1 ⊢ ( 𝑠 = ( 𝑚 𝐻 𝑘 ) → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
178 177 eqeq2d ⊢ ( 𝑠 = ( 𝑚 𝐻 𝑘 ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
179 178 elrab ⊢ ( ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ↔ ( ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
180 176 179 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
181 180 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
182 inss1 ⊢ ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝑚 𝐻 𝑘 )
183 181 182 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ⊆ ( 𝑚 𝐻 𝑘 ) )
184 183 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ⊆ ( 𝑚 𝐻 𝑘 ) )
185 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
186 184 185 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
187 139 140 146 148 186 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
188 187 ex ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) )
189 138 188 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
190 vex ⊢ 𝑥 ∈ V
191 eliin ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) )
192 190 191 ax-mp ⊢ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
193 189 192 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
194 193 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
195 194 ad5ant145 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
196 195 reximdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
197 135 196 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
198 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
199 197 198 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
200 199 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
201 eliin ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
202 190 201 ax-mp ⊢ ( 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
203 200 202 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
204 203 9 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → 𝑥 ∈ 𝐼 )
205 204 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) )
206 205 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) )
207 rabss ⊢ ( { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) )
208 206 207 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐼 )
209 14 208 ssind ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷 ∩ 𝐼 ) )