Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflimlem2 Structured version   Visualization version   GIF version

Theorem smflimlem2 41301
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 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
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
Ref Expression
smflimlem2 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ (𝐷𝐼))
Distinct variable groups:   𝐴,𝑘,𝑚,𝑛   𝐴,𝑠,𝑘,𝑚   𝐶,𝑟   𝐷,𝑘,𝑚,𝑛   𝑛,𝐹,𝑥   𝐹,𝑠,𝑥   𝑘,𝐺,𝑚,𝑛   𝐻,𝑠   𝑥,𝐼   𝑃,𝑟   𝑆,𝑠   𝑘,𝑍,𝑚,𝑛,𝑥   𝜑,𝑘,𝑚,𝑛,𝑥   𝑘,𝑟,𝑚,𝜑
Allowed substitution hints:   𝜑(𝑠)   𝐴(𝑥,𝑟)   𝐶(𝑥,𝑘,𝑚,𝑛,𝑠)   𝐷(𝑥,𝑠,𝑟)   𝑃(𝑥,𝑘,𝑚,𝑛,𝑠)   𝑆(𝑥,𝑘,𝑚,𝑛,𝑟)   𝐹(𝑘,𝑚,𝑟)   𝐺(𝑥,𝑠,𝑟)   𝐻(𝑥,𝑘,𝑚,𝑛,𝑟)   𝐼(𝑘,𝑚,𝑛,𝑠,𝑟)   𝑀(𝑥,𝑘,𝑚,𝑛,𝑠,𝑟)   𝑍(𝑠,𝑟)

Proof of Theorem smflimlem2
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smflimlem2.4 . . . . 5 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
2 nfrab1 3152 . . . . 5 𝑥{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
31, 2nfcxfr 2791 . . . 4 𝑥𝐷
43ssrab2f 39614 . . 3 {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐷
54a1i 11 . 2 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐷)
6 simpllr 815 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥𝐷)
7 ssrab2 3720 . . . . . . . . . . . . . . 15 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
81, 7eqsstri 3668 . . . . . . . . . . . . . 14 𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
98sseli 3632 . . . . . . . . . . . . 13 (𝑥𝐷𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
10 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (ℤ𝑛) = (ℤ𝑖))
1110iineq1d 39581 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑖 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
1211cbviunv 4591 . . . . . . . . . . . . . . 15 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
1312eleq2i 2722 . . . . . . . . . . . . . 14 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ 𝑥 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
14 eliun 4556 . . . . . . . . . . . . . 14 (𝑥 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ↔ ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
1513, 14bitri 264 . . . . . . . . . . . . 13 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
169, 15sylib 208 . . . . . . . . . . . 12 (𝑥𝐷 → ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
176, 16syl 17 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
18 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑚((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴)
19 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑚 𝑘 ∈ ℕ
2018, 19nfan 1868 . . . . . . . . . . . . . . . . . 18 𝑚(((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ)
21 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑚 𝑖𝑍
2220, 21nfan 1868 . . . . . . . . . . . . . . . . 17 𝑚((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍)
23 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑚𝑥
24 nfii1 4583 . . . . . . . . . . . . . . . . . 18 𝑚 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
2523, 24nfel 2806 . . . . . . . . . . . . . . . . 17 𝑚 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
2622, 25nfan 1868 . . . . . . . . . . . . . . . 16 𝑚(((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
27 nfmpt1 4780 . . . . . . . . . . . . . . . 16 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
28 eqid 2651 . . . . . . . . . . . . . . . 16 (ℤ𝑖) = (ℤ𝑖)
29 uzssz 11745 . . . . . . . . . . . . . . . . . . 19 (ℤ𝑀) ⊆ ℤ
30 smflimlem2.1 . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (ℤ𝑀)
3130eleq2i 2722 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑍𝑖 ∈ (ℤ𝑀))
3231biimpi 206 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑍𝑖 ∈ (ℤ𝑀))
3329, 32sseldi 3634 . . . . . . . . . . . . . . . . . 18 (𝑖𝑍𝑖 ∈ ℤ)
34 uzid 11740 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℤ → 𝑖 ∈ (ℤ𝑖))
3533, 34syl 17 . . . . . . . . . . . . . . . . 17 (𝑖𝑍𝑖 ∈ (ℤ𝑖))
3635ad2antlr 763 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝑖 ∈ (ℤ𝑖))
37 simplll 813 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → (𝜑𝑥𝐷))
3837simpld 474 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝜑)
39 uzss 11746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (ℤ𝑀) → (ℤ𝑖) ⊆ (ℤ𝑀))
4032, 39syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖𝑍 → (ℤ𝑖) ⊆ (ℤ𝑀))
4140, 30syl6sseqr 3685 . . . . . . . . . . . . . . . . . . . . 21 (𝑖𝑍 → (ℤ𝑖) ⊆ 𝑍)
4241sselda 3636 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑍𝑚 ∈ (ℤ𝑖)) → 𝑚𝑍)
4342ad4ant24 1327 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑚𝑍)
44 eliinid 39608 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑥 ∈ dom (𝐹𝑚))
4544adantll 750 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑥 ∈ dom (𝐹𝑚))
46 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))
47 fvexd 6241 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚𝑍) → ((𝐹𝑚)‘𝑥) ∈ V)
4846, 47fvmpt2d 6332 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
49483adant3 1101 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
50 smflimlem2.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑆 ∈ SAlg)
5150adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
52 smflimlem2.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
5352ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
54 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 dom (𝐹𝑚) = dom (𝐹𝑚)
5551, 53, 54smff 41262 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
56553adant3 1101 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
57 simp3 1083 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → 𝑥 ∈ dom (𝐹𝑚))
5856, 57ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
5949, 58eqeltrd 2730 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
6038, 43, 45, 59syl3anc 1366 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
6160ad5ant1345 1356 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
6261ad5ant1345 1356 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
631eleq2i 2722 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
6463biimpi 206 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
65 rabidim2 39598 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ )
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐷 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ )
67 climdm 14329 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
6866, 67sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐷 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
6968adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7069, 67sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ )
7170, 67sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
72 nfcv 2793 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐹
73 smflimlem2.5 . . . . . . . . . . . . . . . . . . . 20 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
74 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐷) → 𝑥𝐷)
753, 72, 73, 74fnlimfv 40213 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐷) → (𝐺𝑥) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7675eqcomd 2657 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = (𝐺𝑥))
7771, 76breqtrd 4711 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ (𝐺𝑥))
7877ad4antr 769 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ (𝐺𝑥))
79 smflimlem2.6 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ)
8079ad5antr 773 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝐴 ∈ ℝ)
81 simp-4r 824 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (𝐺𝑥) ≤ 𝐴)
82 simpllr 815 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝑘 ∈ ℕ)
83 nnrecrp 39918 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
8482, 83syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (1 / 𝑘) ∈ ℝ+)
8526, 27, 28, 36, 62, 78, 80, 81, 84climleltrp 40226 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → ∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))))
86 simp-6l 827 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝜑)
87 simplr 807 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝑖𝑍)
8887adantr 480 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑖𝑍)
89 simplr 807 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
90 simpr 476 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑛 ∈ (ℤ𝑖))
91 nfv 1883 . . . . . . . . . . . . . . . . . . . 20 𝑚𝜑
9291, 21, 25nf3an 1871 . . . . . . . . . . . . . . . . . . 19 𝑚(𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
93 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑚 𝑛 ∈ (ℤ𝑖)
9492, 93nfan 1868 . . . . . . . . . . . . . . . . . 18 𝑚((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖))
95 simpll 805 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)))
9628uztrn2 11743 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ𝑖) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑖))
9796adantll 750 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑖))
98 simpll2 1121 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑖𝑍)
99 simplr 807 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚 ∈ (ℤ𝑖))
10098, 99, 42syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚𝑍)
101 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))
102 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚𝑍𝑚𝑍)
103 fvexd 6241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚𝑍 → ((𝐹𝑚)‘𝑥) ∈ V)
104 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
105104fvmpt2 6330 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚𝑍 ∧ ((𝐹𝑚)‘𝑥) ∈ V) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
106102, 103, 105syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚𝑍 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
107106eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚𝑍 → ((𝐹𝑚)‘𝑥) = ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚))
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚𝑍 ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) = ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚))
109 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚𝑍 ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))
110108, 109eqbrtrd 4707 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚𝑍 ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))
111100, 101, 110syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))
112443ad2antl3 1245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑥 ∈ dom (𝐹𝑚))
113112adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ dom (𝐹𝑚))
114 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))
115113, 114jca 553 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))))
116 rabid 3145 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))))
117115, 116sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
118111, 117syldan 486 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
119118adantrl 752 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ (((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
120119ex 449 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12195, 97, 120syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) ∧ 𝑚 ∈ (ℤ𝑛)) → ((((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12294, 121ralimdaa 2987 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → (∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12386, 88, 89, 90, 122syl31anc 1369 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → (∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
124123reximdva 3046 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12585, 124mpd 15 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → ∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
126 ssrexv 3700 . . . . . . . . . . . . . . . 16 ((ℤ𝑖) ⊆ 𝑍 → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12741, 126syl 17 . . . . . . . . . . . . . . 15 (𝑖𝑍 → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
128127ad2antlr 763 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
129125, 128mpd 15 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
130129ex 449 . . . . . . . . . . . 12 (((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) → (𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
131130rexlimdva 3060 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
13217, 131mpd 15 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
133 nfv 1883 . . . . . . . . . . . . . . . 16 𝑚(𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍)
134 nfra1 2970 . . . . . . . . . . . . . . . 16 𝑚𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}
135133, 134nfan 1868 . . . . . . . . . . . . . . 15 𝑚((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
136 simpll1 1120 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
137 simpll2 1121 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
13830uztrn2 11743 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑍𝑗 ∈ (ℤ𝑛)) → 𝑗𝑍)
139138ssd 39566 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
140139sselda 3636 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑍𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
141140adantll 750 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
1421413adantl1 1237 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
143142adantlr 751 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
144 rspa 2959 . . . . . . . . . . . . . . . . . 18 ((∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
145144adantll 750 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
146 simp1 1081 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → 𝜑)
147 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → 𝑚𝑍)
148 simp2 1082 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → 𝑘 ∈ ℕ)
149 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
150149, 50rabexd 4846 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
151150ralrimivw 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ∀𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
152151ralrimivw 2996 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑚𝑍𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
1531523ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → ∀𝑚𝑍𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
154 smflimlem2.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑃 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
155154elrnmpt2id 39741 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚𝑍𝑘 ∈ ℕ ∧ ∀𝑚𝑍𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V) → (𝑚𝑃𝑘) ∈ ran 𝑃)
156147, 148, 153, 155syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝑃𝑘) ∈ ran 𝑃)
157 ovex 6718 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚𝑃𝑘) ∈ V
158 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 = (𝑚𝑃𝑘) → (𝑟 ∈ ran 𝑃 ↔ (𝑚𝑃𝑘) ∈ ran 𝑃))
159158anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑟 = (𝑚𝑃𝑘) → ((𝜑𝑟 ∈ ran 𝑃) ↔ (𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃)))
160 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 = (𝑚𝑃𝑘) → (𝐶𝑟) = (𝐶‘(𝑚𝑃𝑘)))
161 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 = (𝑚𝑃𝑘) → 𝑟 = (𝑚𝑃𝑘))
162160, 161eleq12d 2724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑟 = (𝑚𝑃𝑘) → ((𝐶𝑟) ∈ 𝑟 ↔ (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)))
163159, 162imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 = (𝑚𝑃𝑘) → (((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟) ↔ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))))
164 smflimlem2.10 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
165157, 163, 164vtocl 3290 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))
166146, 156, 165syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))
167 fvexd 6241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ V)
168 smflimlem2.8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))
169168ovmpt4g 6825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚𝑍𝑘 ∈ ℕ ∧ (𝐶‘(𝑚𝑃𝑘)) ∈ V) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘)))
170147, 148, 167, 169syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘)))
171170eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝐶‘(𝑚𝑃𝑘)) = (𝑚𝐻𝑘))
172146, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
173154ovmpt4g 6825 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚𝑍𝑘 ∈ ℕ ∧ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V) → (𝑚𝑃𝑘) = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
174147, 148, 172, 173syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝑃𝑘) = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
175171, 174eleq12d 2724 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → ((𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘) ↔ (𝑚𝐻𝑘) ∈ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}))
176166, 175mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝐻𝑘) ∈ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
177 ineq1 3840 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑚𝐻𝑘) → (𝑠 ∩ dom (𝐹𝑚)) = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚)))
178177eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑚𝐻𝑘) → ({𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚)) ↔ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚))))
179178elrab 3396 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚𝐻𝑘) ∈ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ↔ ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚))))
180176, 179sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚))))
181180simprd 478 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚)))
182 inss1 3866 . . . . . . . . . . . . . . . . . . . 20 ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚)) ⊆ (𝑚𝐻𝑘)
183181, 182syl6eqss 3688 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘))
184183adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘))
185 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
186184, 185sseldd 3637 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ (𝑚𝐻𝑘))
187136, 137, 143, 145, 186syl31anc 1369 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥 ∈ (𝑚𝐻𝑘))
188187ex 449 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → (𝑚 ∈ (ℤ𝑛) → 𝑥 ∈ (𝑚𝐻𝑘)))
189135, 188ralrimi 2986 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ (𝑚𝐻𝑘))
190 vex 3234 . . . . . . . . . . . . . . 15 𝑥 ∈ V
191 eliin 4557 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ (𝑚𝐻𝑘)))
192190, 191ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ (𝑚𝐻𝑘))
193189, 192sylibr 224 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
194193ex 449 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) → (∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
195194ad5ant145 1355 . . . . . . . . . . 11 (((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑛𝑍) → (∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
196195reximdva 3046 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
197132, 196mpd 15 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
198 eliun 4556 . . . . . . . . 9 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
199197, 198sylibr 224 . . . . . . . 8 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
200199ralrimiva 2995 . . . . . . 7 (((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) → ∀𝑘 ∈ ℕ 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
201 eliin 4557 . . . . . . . 8 (𝑥 ∈ V → (𝑥 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
202190, 201ax-mp 5 . . . . . . 7 (𝑥 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
203200, 202sylibr 224 . . . . . 6 (((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) → 𝑥 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
204 smflimlem2.9 . . . . . 6 𝐼 = 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)
205203, 204syl6eleqr 2741 . . . . 5 (((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) → 𝑥𝐼)
206205ex 449 . . . 4 ((𝜑𝑥𝐷) → ((𝐺𝑥) ≤ 𝐴𝑥𝐼))
207206ralrimiva 2995 . . 3 (𝜑 → ∀𝑥𝐷 ((𝐺𝑥) ≤ 𝐴𝑥𝐼))
208 rabss 3712 . . 3 ({𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐼 ↔ ∀𝑥𝐷 ((𝐺𝑥) ≤ 𝐴𝑥𝐼))
209207, 208sylibr 224 . 2 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐼)
2105, 209ssind 3870 1 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ (𝐷𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cin 3606  wss 3607   ciun 4552   ciin 4553   class class class wbr 4685  cmpt 4762  dom cdm 5143  ran crn 5144  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  cr 9973  1c1 9975   + caddc 9977   < clt 10112  cle 10113   / cdiv 10722  cn 11058  cz 11415  cuz 11725  +crp 11870  cli 14259  SAlgcsalg 40846  SMblFncsmblfn 41230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ioo 12217  df-ico 12219  df-fl 12633  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-smblfn 41231
This theorem is referenced by:  smflimlem5  41304
  Copyright terms: Public domain W3C validator