Metamath Proof Explorer

Theorem smflimlem4

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

Proof

Step Hyp Ref Expression
1 smflimlem4.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smflimlem4.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smflimlem4.3 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smflimlem4.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smflimlem4.5 ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
6 smflimlem4.6 ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
7 smflimlem4.7 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
8 smflimlem4.8 ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
9 smflimlem4.9 ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
10 smflimlem4.10 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
11 smflimlem4.11 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
12 inss1 ⊢ ( 𝐷 ∩ 𝐼 ) ⊆ 𝐷
13 12 a1i ⊢ ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ⊆ 𝐷 )
14 13 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → 𝑥 ∈ 𝐷 )
15 6 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
16 nfv ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
17 nfcv ⊢ Ⅎ 𝑚 𝐹
18 nfcv ⊢ Ⅎ 𝑧 𝐹
19 3 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
20 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
21 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
22 19 20 21 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
23 22 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
24 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
25 24 mpteq2dv ⊢ ( 𝑥 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
26 25 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ∈ dom ⇝ ) )
27 26 cbvrabv ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑧 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ∈ dom ⇝ }
28 5 27 eqtri ⊢ 𝐷 = { 𝑧 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ∈ dom ⇝ }
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
30 16 17 18 2 23 28 29 fnlimfvre ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
31 30 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ V )
32 15 31 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
33 32 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
34 14 33 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
36 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
37 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
39 36 38 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 + 𝑦 ) ∈ ℝ )
40 39 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 + 𝑦 ) ∈ ℝ )
41 nfv ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ )
42 rphalfcl ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
43 rpgtrecnn ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
44 42 43 syl ⊢ ( 𝑦 ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
46 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝑆 ∈ SAlg )
47 20 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
48 47 ad5ant15 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
49 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → 𝐴 ∈ ℝ )
50 49 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝐴 ∈ ℝ )
51 nfcv ⊢ Ⅎ 𝑘 𝑍
52 nfcv ⊢ Ⅎ 𝑗 𝑍
53 nfcv ⊢ Ⅎ 𝑗 { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
54 nfcv ⊢ Ⅎ 𝑘 { 𝑠 ∈ 𝑆 ∣ { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
55 24 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
56 55 cbvrabv ⊢ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) }
57 56 a1i ⊢ ( 𝑘 = 𝑗 → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
58 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 1 / 𝑘 ) = ( 1 / 𝑗 ) )
59 58 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 + ( 1 / 𝑘 ) ) = ( 𝐴 + ( 1 / 𝑗 ) ) )
60 59 breq2d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) ) )
61 60 rabbidv ⊢ ( 𝑘 = 𝑗 → { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } )
62 57 61 eqtrd ⊢ ( 𝑘 = 𝑗 → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } )
63 62 eqeq1d ⊢ ( 𝑘 = 𝑗 → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
64 63 rabbidv ⊢ ( 𝑘 = 𝑗 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
65 51 52 53 54 64 cbvmpo2 ⊢ ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) = ( 𝑚 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
66 8 65 eqtri ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑧 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
67 nfcv ⊢ Ⅎ 𝑗 ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) )
68 nfcv ⊢ Ⅎ 𝑘 ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) )
69 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑚 𝑃 𝑘 ) = ( 𝑚 𝑃 𝑗 ) )
70 69 fveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) ) )
71 51 52 67 68 70 cbvmpo2 ⊢ ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) = ( 𝑚 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) ) )
72 9 71 eqtri ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) ) )
73 simpll ⊢ ( ( ( 𝑘 = 𝑗 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 = 𝑗 )
74 73 oveq2d ⊢ ( ( ( 𝑘 = 𝑗 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑚 𝐻 𝑘 ) = ( 𝑚 𝐻 𝑗 ) )
75 74 iineq2dv ⊢ ( ( 𝑘 = 𝑗 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑗 ) )
76 75 iuneq2dv ⊢ ( 𝑘 = 𝑗 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑗 ) )
77 76 cbviinv ⊢ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑗 )
78 10 77 eqtri ⊢ 𝐼 = ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑗 )
79 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
80 79 ad5ant15 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
81 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) )
82 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝑘 ∈ ℕ )
83 42 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → ( 𝑦 / 2 ) ∈ ℝ+ )
84 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
85 2 46 48 28 50 66 72 78 80 81 82 83 84 smflimlem3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
86 85 rexlimdva2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) )
87 45 86 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
88 nfv ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ )
89 nfcv ⊢ Ⅎ 𝑖 𝐹
90 nfcv ⊢ Ⅎ 𝑥 𝐹
91 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
92 eleq1w ⊢ ( 𝑚 = 𝑖 → ( 𝑚 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍 ) )
93 92 anbi2d ⊢ ( 𝑚 = 𝑖 → ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ) )
94 fveq2 ⊢ ( 𝑚 = 𝑖 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑖 ) )
95 94 dmeqd ⊢ ( 𝑚 = 𝑖 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑖 ) )
96 94 95 feq12d ⊢ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ↔ ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ ) )
97 93 96 imbi12d ⊢ ( 𝑚 = 𝑖 → ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ ) ) )
98 97 22 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ )
99 98 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ )
100 fveq2 ⊢ ( 𝑚 = 𝑙 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑙 ) )
101 100 dmeqd ⊢ ( 𝑚 = 𝑙 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑙 ) )
102 101 cbviinv ⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 )
103 102 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) )
104 103 iuneq2i ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 )
105 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑚 ) )
106 105 iineq1d ⊢ ( 𝑛 = 𝑚 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑙 ) )
107 fveq2 ⊢ ( 𝑙 = 𝑖 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑖 ) )
108 107 dmeqd ⊢ ( 𝑙 = 𝑖 → dom ( 𝐹 ‘ 𝑙 ) = dom ( 𝐹 ‘ 𝑖 ) )
109 108 cbviinv ⊢ ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 )
110 109 a1i ⊢ ( 𝑛 = 𝑚 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) )
111 106 110 eqtrd ⊢ ( 𝑛 = 𝑚 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) )
112 111 cbviunv ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 )
113 104 112 eqtri ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 )
114 113 rabeqi ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
115 fveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑚 ) )
116 115 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
117 116 cbvmptv ⊢ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
118 117 eqcomi ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) )
119 118 eleq1i ⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
120 119 rabbii ⊢ { 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) ∣ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
121 5 114 120 3eqtri ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) ∣ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
122 118 fveq2i ⊢ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) )
123 122 mpteq2i ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
124 6 123 eqtri ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
125 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑥 ∈ 𝐷 )
126 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ+ )
127 88 89 90 91 2 99 121 124 125 126 fnlimabslt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) )
128 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
129 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ )
130 128 129 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ ℝ )
131 130 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ ℝ )
132 130 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ ℂ )
133 132 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) ∈ ℝ )
134 133 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) ∈ ℝ )
135 37 rehalfcld ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
136 135 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( 𝑦 / 2 ) ∈ ℝ )
137 131 leabsd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
138 34 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
140 recn ⊢ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
141 140 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
142 139 141 abssubd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
143 142 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
144 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) )
145 143 144 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) )
146 145 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) )
147 131 134 136 137 146 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) < ( 𝑦 / 2 ) )
148 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
149 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ )
150 148 149 136 ltsubadd2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( ( 𝐺 ‘ 𝑥 ) − ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) < ( 𝑦 / 2 ) ↔ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
151 147 150 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
152 151 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
153 152 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
154 153 ralimdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
155 154 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑚 ∈ 𝑍 → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ) )
156 41 155 reximdai ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
157 127 156 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
158 115 dmeqd ⊢ ( 𝑖 = 𝑚 → dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) )
159 158 eleq2d ⊢ ( 𝑖 = 𝑚 → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ↔ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) )
160 116 breq1d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
161 159 160 anbi12d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) )
162 116 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) = ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
163 162 breq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ↔ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
164 41 2 87 157 161 163 rexanuz3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚 ∈ 𝑍 ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
165 df-3an ⊢ ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
166 3ancomb ⊢ ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
167 165 166 bitr3i ⊢ ( ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
168 167 rexbii ⊢ ( ∃ 𝑚 ∈ 𝑍 ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ∃ 𝑚 ∈ 𝑍 ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
169 164 168 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚 ∈ 𝑍 ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
170 35 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
171 22 3adant3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
172 simp3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
173 171 172 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
174 173 ad4ant134 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
175 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑦 ∈ ℝ+ )
176 175 135 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑦 / 2 ) ∈ ℝ )
177 174 176 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∈ ℝ )
178 177 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∈ ℝ )
179 178 3ad2antr1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∈ ℝ )
180 rehalfcl ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 / 2 ) ∈ ℝ )
181 38 180 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ )
182 36 181 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) )
183 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 𝑦 / 2 ) ) ∈ ℝ )
184 182 183 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 + ( 𝑦 / 2 ) ) ∈ ℝ )
185 184 181 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) ∈ ℝ )
186 185 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) ∈ ℝ )
187 simpr2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
188 174 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
189 184 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐴 + ( 𝑦 / 2 ) ) ∈ ℝ )
190 176 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝑦 / 2 ) ∈ ℝ )
191 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) )
192 188 189 190 191 ltadd1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
193 192 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
194 193 3adantr2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
195 170 179 186 187 194 lttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
196 36 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
197 181 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℂ )
198 196 197 197 addassd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝐴 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
199 37 recnd ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
200 2halves ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
201 199 200 syl ⊢ ( 𝑦 ∈ ℝ+ → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
202 201 oveq2d ⊢ ( 𝑦 ∈ ℝ+ → ( 𝐴 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( 𝐴 + 𝑦 ) )
203 202 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( 𝐴 + 𝑦 ) )
204 198 203 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝐴 + 𝑦 ) )
205 204 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝐴 + 𝑦 ) )
206 195 205 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) < ( 𝐴 + 𝑦 ) )
207 206 rexlimdva2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ 𝑍 ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑥 ) < ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) → ( 𝐺 ‘ 𝑥 ) < ( 𝐴 + 𝑦 ) ) )
208 169 207 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐺 ‘ 𝑥 ) < ( 𝐴 + 𝑦 ) )
209 35 40 208 ltled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐴 + 𝑦 ) )
210 209 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → ∀ 𝑦 ∈ ℝ+ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐴 + 𝑦 ) )
211 alrple ⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ℝ+ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐴 + 𝑦 ) ) )
212 34 49 211 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ℝ+ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐴 + 𝑦 ) ) )
213 210 212 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 ∩ 𝐼 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
214 13 213 ssrabdv ⊢ ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ⊆ { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } )