Metamath Proof Explorer

Theorem smflimlem3

Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflimlem3.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimlem3.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimlem3.m ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
smflimlem3.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
smflimlem3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
smflimlem3.p ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
smflimlem3.h ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
smflimlem3.i ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
smflimlem3.c ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 )
smflimlem3.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∩ 𝐼 ) )
smflimlem3.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
smflimlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
smflimlem3.l ⊢ ( 𝜑 → ( 1 / 𝐾 ) < 𝑌 )
Assertion smflimlem3 ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 smflimlem3.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 smflimlem3.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3 smflimlem3.m ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
4 smflimlem3.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
5 smflimlem3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 smflimlem3.p ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
7 smflimlem3.h ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
8 smflimlem3.i ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
9 smflimlem3.c ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 )
10 smflimlem3.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∩ 𝐼 ) )
11 smflimlem3.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
12 smflimlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
13 smflimlem3.l ⊢ ( 𝜑 → ( 1 / 𝐾 ) < 𝑌 )
14 ssrab2 ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
15 4 14 eqsstri ⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
16 inss1 ⊢ ( 𝐷 ∩ 𝐼 ) ⊆ 𝐷
17 16 10 sseldi ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
18 15 17 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
19 fveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑚 ) )
20 19 dmeqd ⊢ ( 𝑖 = 𝑚 → dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) )
21 eqcom ⊢ ( 𝑖 = 𝑚 ↔ 𝑚 = 𝑖 )
22 21 imbi1i ⊢ ( ( 𝑖 = 𝑚 → dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) ) ↔ ( 𝑚 = 𝑖 → dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) ) )
23 eqcom ⊢ ( dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) ↔ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑖 ) )
24 23 imbi2i ⊢ ( ( 𝑚 = 𝑖 → dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) ) ↔ ( 𝑚 = 𝑖 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑖 ) ) )
25 22 24 bitri ⊢ ( ( 𝑖 = 𝑚 → dom ( 𝐹 ‘ 𝑖 ) = dom ( 𝐹 ‘ 𝑚 ) ) ↔ ( 𝑚 = 𝑖 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑖 ) ) )
26 20 25 mpbi ⊢ ( 𝑚 = 𝑖 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑖 ) )
27 26 cbviinv ⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑖 )
28 27 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑖 ) )
29 28 iuneq2i ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑖 )
30 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑚 ) )
31 30 iineq1d ⊢ ( 𝑛 = 𝑚 → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑖 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) )
32 31 cbviunv ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑖 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 )
33 29 32 eqtri ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 )
34 18 33 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) )
35 eqid ⊢ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 )
36 1 35 allbutfi ⊢ ( 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) ↔ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) )
37 36 biimpi ⊢ ( 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) dom ( 𝐹 ‘ 𝑖 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) )
38 34 37 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) )
39 10 elin2d ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
40 oveq1 ⊢ ( 𝑚 = 𝑖 → ( 𝑚 𝐻 𝑘 ) = ( 𝑖 𝐻 𝑘 ) )
41 40 cbviinv ⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 𝐻 𝑘 )
42 41 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 𝐻 𝑘 ) )
43 42 iuneq2i ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 𝐻 𝑘 )
44 30 iineq1d ⊢ ( 𝑛 = 𝑚 → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 𝐻 𝑘 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 ) )
45 44 cbviunv ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 𝐻 𝑘 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 )
46 43 45 eqtri ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 )
47 46 a1i ⊢ ( 𝑘 ∈ ℕ → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 ) )
48 47 iineq2i ⊢ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) = ∩ 𝑘 ∈ ℕ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 )
49 8 48 eqtri ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 )
50 39 49 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 ) )
51 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑖 𝐻 𝑘 ) = ( 𝑖 𝐻 𝐾 ) )
52 51 adantr ⊢ ( ( 𝑘 = 𝐾 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( 𝑖 𝐻 𝑘 ) = ( 𝑖 𝐻 𝐾 ) )
53 52 iineq2dv ⊢ ( 𝑘 = 𝐾 → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 ) )
54 53 iuneq2d ⊢ ( 𝑘 = 𝐾 → ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 ) )
55 54 eleq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝑘 ) ↔ 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 ) ) )
56 50 11 55 eliind ⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 ) )
57 eqid ⊢ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 ) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 )
58 1 57 allbutfi ⊢ ( 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑖 𝐻 𝐾 ) ↔ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) )
59 56 58 sylib ⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) )
60 38 59 jca ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) )
61 1 rexanuz2 ⊢ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ↔ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) )
62 60 61 sylibr ⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) )
63 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝜑 )
64 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
65 1 uztrn2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑖 ∈ 𝑍 )
66 64 65 sylan ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑖 ∈ 𝑍 )
67 simprl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) )
68 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) )
69 7 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) )
70 oveq12 ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( 𝑚 𝑃 𝑘 ) = ( 𝑖 𝑃 𝐾 ) )
71 70 fveq2d ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
74 11 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐾 ∈ ℕ )
75 fvexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ V )
76 69 72 73 74 75 ovmpod ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 𝐻 𝐾 ) = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
77 76 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → ( 𝑖 𝐻 𝐾 ) = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
78 68 77 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → 𝑋 ∈ ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
79 78 3expa ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → 𝑋 ∈ ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
80 79 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → 𝑋 ∈ ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
81 80 67 elind ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → 𝑋 ∈ ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) )
82 eqid ⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
83 82 2 rabexd ⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
84 83 ralrimivw ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
85 84 a1d ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) )
86 85 imp ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
87 86 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
88 6 fnmpo ⊢ ( ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V → 𝑃 Fn ( 𝑍 × ℕ ) )
89 87 88 syl ⊢ ( 𝜑 → 𝑃 Fn ( 𝑍 × ℕ ) )
90 89 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑃 Fn ( 𝑍 × ℕ ) )
91 fnovrn ⊢ ( ( 𝑃 Fn ( 𝑍 × ℕ ) ∧ 𝑖 ∈ 𝑍 ∧ 𝐾 ∈ ℕ ) → ( 𝑖 𝑃 𝐾 ) ∈ ran 𝑃 )
92 90 73 74 91 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 𝑃 𝐾 ) ∈ ran 𝑃 )
93 ovex ⊢ ( 𝑖 𝑃 𝐾 ) ∈ V
94 eleq1 ⊢ ( 𝑦 = ( 𝑖 𝑃 𝐾 ) → ( 𝑦 ∈ ran 𝑃 ↔ ( 𝑖 𝑃 𝐾 ) ∈ ran 𝑃 ) )
95 94 anbi2d ⊢ ( 𝑦 = ( 𝑖 𝑃 𝐾 ) → ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) ↔ ( 𝜑 ∧ ( 𝑖 𝑃 𝐾 ) ∈ ran 𝑃 ) ) )
96 fveq2 ⊢ ( 𝑦 = ( 𝑖 𝑃 𝐾 ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) )
97 id ⊢ ( 𝑦 = ( 𝑖 𝑃 𝐾 ) → 𝑦 = ( 𝑖 𝑃 𝐾 ) )
98 96 97 eleq12d ⊢ ( 𝑦 = ( 𝑖 𝑃 𝐾 ) → ( ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ ( 𝑖 𝑃 𝐾 ) ) )
99 95 98 imbi12d ⊢ ( 𝑦 = ( 𝑖 𝑃 𝐾 ) → ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( ( 𝜑 ∧ ( 𝑖 𝑃 𝐾 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ ( 𝑖 𝑃 𝐾 ) ) ) )
100 93 99 9 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑖 𝑃 𝐾 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ ( 𝑖 𝑃 𝐾 ) )
101 92 100 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ ( 𝑖 𝑃 𝐾 ) )
102 6 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
103 26 adantr ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑖 ) )
104 19 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
105 21 imbi1i ⊢ ( ( 𝑖 = 𝑚 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ↔ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
106 eqcom ⊢ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) )
107 106 imbi2i ⊢ ( ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ↔ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) )
108 105 107 bitri ⊢ ( ( 𝑖 = 𝑚 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ↔ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) )
109 104 108 mpbi ⊢ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) )
110 109 adantr ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) )
111 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 1 / 𝑘 ) = ( 1 / 𝐾 ) )
112 111 oveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐴 + ( 1 / 𝑘 ) ) = ( 𝐴 + ( 1 / 𝐾 ) ) )
113 112 adantl ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( 𝐴 + ( 1 / 𝑘 ) ) = ( 𝐴 + ( 1 / 𝐾 ) ) )
114 110 113 breq12d ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ↔ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) )
115 103 114 rabeqbidv ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } )
116 26 ineq2d ⊢ ( 𝑚 = 𝑖 → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) )
117 116 adantr ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) )
118 115 117 eqeq12d ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) ) )
119 118 rabbidv ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } )
120 119 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑚 = 𝑖 ∧ 𝑘 = 𝐾 ) ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } )
121 eqid ⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) }
122 121 2 rabexd ⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } ∈ V )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } ∈ V )
124 102 120 73 74 123 ovmpod ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 𝑃 𝐾 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } )
125 101 124 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } )
126 ineq1 ⊢ ( 𝑠 = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) )
127 126 eqeq2d ⊢ ( 𝑠 = ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) ) )
128 127 elrab ⊢ ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑖 ) ) } ↔ ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) ) )
129 125 128 sylib ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) ) )
130 129 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } = ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) )
131 130 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → ( ( 𝐶 ‘ ( 𝑖 𝑃 𝐾 ) ) ∩ dom ( 𝐹 ‘ 𝑖 ) ) = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } )
133 81 132 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → 𝑋 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } )
134 fveq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) )
135 eqidd ⊢ ( 𝑥 = 𝑋 → ( 𝐴 + ( 1 / 𝐾 ) ) = ( 𝐴 + ( 1 / 𝐾 ) ) )
136 134 135 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ↔ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) )
137 136 elrab ⊢ ( 𝑋 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑖 ) ∣ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝐾 ) ) } ↔ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) )
138 133 137 sylib ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) )
139 138 simprd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) )
140 67 139 jca ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) )
141 140 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) )
142 63 66 141 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) )
143 142 ralimdva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) )
144 143 reximdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ 𝑋 ∈ ( 𝑖 𝐻 𝐾 ) ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) )
145 62 144 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) )
146 simprl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) )
147 eleq1 ⊢ ( 𝑚 = 𝑖 → ( 𝑚 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍 ) )
148 147 anbi2d ⊢ ( 𝑚 = 𝑖 → ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ) )
149 fveq2 ⊢ ( 𝑚 = 𝑖 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑖 ) )
150 149 26 feq12d ⊢ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ↔ ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ ) )
151 148 150 imbi12d ⊢ ( 𝑚 = 𝑖 → ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ ) ) )
152 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
153 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
154 152 3 153 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
155 151 154 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ )
156 155 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑖 ) : dom ( 𝐹 ‘ 𝑖 ) ⟶ ℝ )
157 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ) → 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) )
158 156 157 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) ∈ ℝ )
159 158 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) ∈ ℝ )
160 11 nnrecred ⊢ ( 𝜑 → ( 1 / 𝐾 ) ∈ ℝ )
161 5 160 readdcld ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 𝐾 ) ) ∈ ℝ )
162 161 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( 𝐴 + ( 1 / 𝐾 ) ) ∈ ℝ )
163 12 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
164 5 163 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝑌 ) ∈ ℝ )
165 164 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( 𝐴 + 𝑌 ) ∈ ℝ )
166 simprr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) )
167 160 163 5 13 ltadd2dd ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 𝐾 ) ) < ( 𝐴 + 𝑌 ) )
168 167 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( 𝐴 + ( 1 / 𝐾 ) ) < ( 𝐴 + 𝑌 ) )
169 159 162 165 166 168 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) )
170 146 169 jca ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) )
171 170 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) ) )
172 63 66 171 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) ) )
173 172 ralimdva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) ) )
174 173 reximdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + ( 1 / 𝐾 ) ) ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) ) )
175 145 174 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑖 ) ∧ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑋 ) < ( 𝐴 + 𝑌 ) ) )