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 ffvelrnda ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
60 eqid dom ( 𝐹𝑚 ) = dom ( 𝐹𝑚 )
61 58 59 60 smff ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
62 61 3adant3 ( ( 𝜑𝑚𝑍𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
63 simp3 ( ( 𝜑𝑚𝑍𝑥 ∈ dom ( 𝐹𝑚 ) ) → 𝑥 ∈ dom ( 𝐹𝑚 ) )
64 62 63 ffvelrnd ( ( 𝜑𝑚𝑍𝑥 ∈ 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 ( 𝜑 → { 𝑥𝐷 ∣ ( 𝐺𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷𝐼 ) )