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 46162
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 3448 . . . . 5 𝑥{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
31, 2nfcxfr 2896 . . . 4 𝑥𝐷
43ssrab2f 44486 . . 3 {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐷
54a1i 11 . 2 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐷)
6 simpllr 774 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥𝐷)
7 ssrab2 4075 . . . . . . . . . . . . . . 15 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
81, 7eqsstri 4014 . . . . . . . . . . . . . 14 𝐷 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
98sseli 3976 . . . . . . . . . . . . 13 (𝑥𝐷𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
10 fveq2 6900 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (ℤ𝑛) = (ℤ𝑖))
1110iineq1d 44459 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑖 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
1211cbviunv 5045 . . . . . . . . . . . . . . 15 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
1312eleq2i 2820 . . . . . . . . . . . . . 14 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ 𝑥 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
14 eliun 5002 . . . . . . . . . . . . . 14 (𝑥 𝑖𝑍 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ↔ ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
1513, 14bitri 274 . . . . . . . . . . . . 13 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
169, 15sylib 217 . . . . . . . . . . . 12 (𝑥𝐷 → ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
176, 16syl 17 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
18 nfv 1909 . . . . . . . . . . . . . . . . . 18 𝑚((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴)
19 nfv 1909 . . . . . . . . . . . . . . . . . 18 𝑚 𝑘 ∈ ℕ
2018, 19nfan 1894 . . . . . . . . . . . . . . . . 17 𝑚(((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ)
21 nfv 1909 . . . . . . . . . . . . . . . . 17 𝑚 𝑖𝑍
2220, 21nfan 1894 . . . . . . . . . . . . . . . 16 𝑚((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍)
23 nfcv 2898 . . . . . . . . . . . . . . . . 17 𝑚𝑥
24 nfii1 5034 . . . . . . . . . . . . . . . . 17 𝑚 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
2523, 24nfel 2913 . . . . . . . . . . . . . . . 16 𝑚 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)
2622, 25nfan 1894 . . . . . . . . . . . . . . 15 𝑚(((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
27 nfmpt1 5258 . . . . . . . . . . . . . . 15 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
28 eqid 2727 . . . . . . . . . . . . . . 15 (ℤ𝑖) = (ℤ𝑖)
29 uzssz 12879 . . . . . . . . . . . . . . . . . 18 (ℤ𝑀) ⊆ ℤ
30 smflimlem2.1 . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
3130eleq2i 2820 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑍𝑖 ∈ (ℤ𝑀))
3231biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑖𝑍𝑖 ∈ (ℤ𝑀))
3329, 32sselid 3978 . . . . . . . . . . . . . . . . 17 (𝑖𝑍𝑖 ∈ ℤ)
34 uzid 12873 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℤ → 𝑖 ∈ (ℤ𝑖))
3533, 34syl 17 . . . . . . . . . . . . . . . 16 (𝑖𝑍𝑖 ∈ (ℤ𝑖))
3635ad2antlr 725 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝑖 ∈ (ℤ𝑖))
37 simplll 773 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → (𝜑𝑥𝐷))
3837simpld 493 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝜑)
39 uzss 12881 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (ℤ𝑀) → (ℤ𝑖) ⊆ (ℤ𝑀))
4032, 39syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑖𝑍 → (ℤ𝑖) ⊆ (ℤ𝑀))
4140, 30sseqtrrdi 4031 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑍 → (ℤ𝑖) ⊆ 𝑍)
4241sselda 3980 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑍𝑚 ∈ (ℤ𝑖)) → 𝑚𝑍)
4342ad4ant24 752 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑚𝑍)
44 eliinid 44480 . . . . . . . . . . . . . . . . . . 19 ((𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑥 ∈ dom (𝐹𝑚))
4544adantll 712 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑥 ∈ dom (𝐹𝑚))
46 eqidd 2728 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))
47 fvexd 6915 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → ((𝐹𝑚)‘𝑥) ∈ V)
4846, 47fvmpt2d 7021 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
49483adant3 1129 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
50 smflimlem2.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆 ∈ SAlg)
5150adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
52 smflimlem2.3 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
5352ffvelcdmda 7097 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
54 eqid 2727 . . . . . . . . . . . . . . . . . . . . . 22 dom (𝐹𝑚) = dom (𝐹𝑚)
5551, 53, 54smff 46122 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
56553adant3 1129 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
57 simp3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → 𝑥 ∈ dom (𝐹𝑚))
5856, 57ffvelcdmd 7098 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
5949, 58eqeltrd 2828 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
6038, 43, 45, 59syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥𝐷) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
6160adantl3r 748 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
6261adantl3r 748 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ)
631eleq2i 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
6463biimpi 215 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ })
65 rabidim2 44471 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ )
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐷 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ )
67 climdm 15536 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
6866, 67sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐷 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
6968adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7069, 67sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ )
7170, 67sylib 217 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
72 nfcv 2898 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
73 smflimlem2.5 . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
74 simpr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐷) → 𝑥𝐷)
753, 72, 73, 74fnlimfv 45053 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → (𝐺𝑥) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7675eqcomd 2733 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = (𝐺𝑥))
7771, 76breqtrd 5176 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐷) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ (𝐺𝑥))
7877ad4antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ⇝ (𝐺𝑥))
79 smflimlem2.6 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ)
8079ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝐴 ∈ ℝ)
81 simp-4r 782 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (𝐺𝑥) ≤ 𝐴)
82 simpllr 774 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝑘 ∈ ℕ)
83 nnrecrp 44770 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
8482, 83syl 17 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (1 / 𝑘) ∈ ℝ+)
8526, 27, 28, 36, 62, 78, 80, 81, 84climleltrp 45066 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → ∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))))
86 simp-6l 785 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝜑)
87 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → 𝑖𝑍)
8887adantr 479 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑖𝑍)
89 simplr 767 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
90 simpr 483 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑛 ∈ (ℤ𝑖))
91 nfv 1909 . . . . . . . . . . . . . . . . . . 19 𝑚𝜑
9291, 21, 25nf3an 1896 . . . . . . . . . . . . . . . . . 18 𝑚(𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚))
93 nfv 1909 . . . . . . . . . . . . . . . . . 18 𝑚 𝑛 ∈ (ℤ𝑖)
9492, 93nfan 1894 . . . . . . . . . . . . . . . . 17 𝑚((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖))
95 simpll 765 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)))
9628uztrn2 12877 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ𝑖) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑖))
9796adantll 712 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑖))
98 simpll2 1210 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑖𝑍)
99 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚 ∈ (ℤ𝑖))
10098, 99, 42syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚𝑍)
101 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))
102 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚𝑍𝑚𝑍)
103 fvexd 6915 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚𝑍 → ((𝐹𝑚)‘𝑥) ∈ V)
104 eqid 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
105104fvmpt2 7019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚𝑍 ∧ ((𝐹𝑚)‘𝑥) ∈ V) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
106102, 103, 105syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚𝑍 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) = ((𝐹𝑚)‘𝑥))
107106eqcomd 2733 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚𝑍 → ((𝐹𝑚)‘𝑥) = ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚))
108107adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚𝑍 ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) = ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚))
109 simpr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚𝑍 ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))
110108, 109eqbrtrd 5172 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚𝑍 ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))
111100, 101, 110syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))
112443ad2antl3 1184 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → 𝑥 ∈ dom (𝐹𝑚))
113112adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ dom (𝐹𝑚))
114 simpr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))
115113, 114jca 510 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))))
116 rabid 3449 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))))
117115, 116sylibr 233 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
118111, 117syldan 589 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
119118adantrl 714 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) ∧ (((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
120119ex 411 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑚 ∈ (ℤ𝑖)) → ((((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12195, 97, 120syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) ∧ 𝑚 ∈ (ℤ𝑛)) → ((((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12294, 121ralimdaa 3253 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝑍𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → (∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12386, 88, 89, 90, 122syl31anc 1370 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) ∧ 𝑛 ∈ (ℤ𝑖)) → (∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
124123reximdva 3164 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)(((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12585, 124mpd 15 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → ∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
126 ssrexv 4049 . . . . . . . . . . . . . . 15 ((ℤ𝑖) ⊆ 𝑍 → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
12741, 126syl 17 . . . . . . . . . . . . . 14 (𝑖𝑍 → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
128127ad2antlr 725 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → (∃𝑛 ∈ (ℤ𝑖)∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
129125, 128mpd 15 . . . . . . . . . . . 12 ((((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖𝑍) ∧ 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚)) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
130129rexlimdva2 3153 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑖𝑍 𝑥 𝑚 ∈ (ℤ𝑖)dom (𝐹𝑚) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}))
13117, 130mpd 15 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
132 nfv 1909 . . . . . . . . . . . . . . . 16 𝑚(𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍)
133 nfra1 3277 . . . . . . . . . . . . . . . 16 𝑚𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}
134132, 133nfan 1894 . . . . . . . . . . . . . . 15 𝑚((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
135 simpll1 1209 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
136 simpll2 1210 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
13730uztrn2 12877 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑍𝑗 ∈ (ℤ𝑛)) → 𝑗𝑍)
138137ssd 44449 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
139138sselda 3980 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑍𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
140139adantll 712 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
1411403adantl1 1163 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
142141adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
143 rspa 3241 . . . . . . . . . . . . . . . . . 18 ((∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
144143adantll 712 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
145 simp1 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → 𝜑)
146 simp3 1135 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → 𝑚𝑍)
147 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → 𝑘 ∈ ℕ)
148 eqid 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
149148, 50rabexd 5337 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
150149ralrimivw 3146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ∀𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
151150ralrimivw 3146 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑚𝑍𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
1521513ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → ∀𝑚𝑍𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
153 smflimlem2.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑃 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
154153elrnmpoid 44604 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚𝑍𝑘 ∈ ℕ ∧ ∀𝑚𝑍𝑘 ∈ ℕ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V) → (𝑚𝑃𝑘) ∈ ran 𝑃)
155146, 147, 152, 154syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝑃𝑘) ∈ ran 𝑃)
156 ovex 7457 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚𝑃𝑘) ∈ V
157 eleq1 2816 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 = (𝑚𝑃𝑘) → (𝑟 ∈ ran 𝑃 ↔ (𝑚𝑃𝑘) ∈ ran 𝑃))
158157anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑟 = (𝑚𝑃𝑘) → ((𝜑𝑟 ∈ ran 𝑃) ↔ (𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃)))
159 fveq2 6900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 = (𝑚𝑃𝑘) → (𝐶𝑟) = (𝐶‘(𝑚𝑃𝑘)))
160 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 = (𝑚𝑃𝑘) → 𝑟 = (𝑚𝑃𝑘))
161159, 160eleq12d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑟 = (𝑚𝑃𝑘) → ((𝐶𝑟) ∈ 𝑟 ↔ (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)))
162158, 161imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 = (𝑚𝑃𝑘) → (((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟) ↔ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))))
163 smflimlem2.10 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
164156, 162, 163vtocl 3543 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))
165145, 155, 164syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))
166 fvexd 6915 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ V)
167 smflimlem2.8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))
168167ovmpt4g 7572 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚𝑍𝑘 ∈ ℕ ∧ (𝐶‘(𝑚𝑃𝑘)) ∈ V) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘)))
169146, 147, 166, 168syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘)))
170169eqcomd 2733 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝐶‘(𝑚𝑃𝑘)) = (𝑚𝐻𝑘))
171145, 149syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V)
172153ovmpt4g 7572 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚𝑍𝑘 ∈ ℕ ∧ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ∈ V) → (𝑚𝑃𝑘) = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
173146, 147, 171, 172syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝑃𝑘) = {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
174170, 173eleq12d 2822 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → ((𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘) ↔ (𝑚𝐻𝑘) ∈ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}))
175165, 174mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → (𝑚𝐻𝑘) ∈ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
176 ineq1 4205 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑚𝐻𝑘) → (𝑠 ∩ dom (𝐹𝑚)) = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚)))
177176eqeq2d 2738 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑚𝐻𝑘) → ({𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚)) ↔ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚))))
178177elrab 3682 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚𝐻𝑘) ∈ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} ↔ ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚))))
179175, 178sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚))))
180179simprd 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚)))
181 inss1 4229 . . . . . . . . . . . . . . . . . . . 20 ((𝑚𝐻𝑘) ∩ dom (𝐹𝑚)) ⊆ (𝑚𝐻𝑘)
182180, 181eqsstrdi 4034 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘))
183182adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘))
184 simpr 483 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})
185183, 184sseldd 3981 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ ∧ 𝑚𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ (𝑚𝐻𝑘))
186135, 136, 142, 144, 185syl31anc 1370 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥 ∈ (𝑚𝐻𝑘))
187186ex 411 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → (𝑚 ∈ (ℤ𝑛) → 𝑥 ∈ (𝑚𝐻𝑘)))
188134, 187ralrimi 3250 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ (𝑚𝐻𝑘))
189 vex 3475 . . . . . . . . . . . . . . 15 𝑥 ∈ V
190 eliin 5003 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ (𝑚𝐻𝑘)))
191189, 190ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ (𝑚𝐻𝑘))
192188, 191sylibr 233 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) ∧ ∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
193192ex 411 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ ∧ 𝑛𝑍) → (∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
194193ad5ant145 1366 . . . . . . . . . . 11 (((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑛𝑍) → (∀𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
195194reximdva 3164 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑛𝑍𝑚 ∈ (ℤ𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
196131, 195mpd 15 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
197 eliun 5002 . . . . . . . . 9 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
198196, 197sylibr 233 . . . . . . . 8 ((((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
199198ralrimiva 3142 . . . . . . 7 (((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) → ∀𝑘 ∈ ℕ 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
200 eliin 5003 . . . . . . . 8 (𝑥 ∈ V → (𝑥 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)))
201189, 200ax-mp 5 . . . . . . 7 (𝑥 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
202199, 201sylibr 233 . . . . . 6 (((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) → 𝑥 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘))
203 smflimlem2.9 . . . . . 6 𝐼 = 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)
204202, 203eleqtrrdi 2839 . . . . 5 (((𝜑𝑥𝐷) ∧ (𝐺𝑥) ≤ 𝐴) → 𝑥𝐼)
205204ex 411 . . . 4 ((𝜑𝑥𝐷) → ((𝐺𝑥) ≤ 𝐴𝑥𝐼))
206205ralrimiva 3142 . . 3 (𝜑 → ∀𝑥𝐷 ((𝐺𝑥) ≤ 𝐴𝑥𝐼))
207 rabss 4067 . . 3 ({𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐼 ↔ ∀𝑥𝐷 ((𝐺𝑥) ≤ 𝐴𝑥𝐼))
208206, 207sylibr 233 . 2 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ 𝐼)
2095, 208ssind 4233 1 (𝜑 → {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴} ⊆ (𝐷𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3057  wrex 3066  {crab 3428  Vcvv 3471  cin 3946  wss 3947   ciun 4998   ciin 4999   class class class wbr 5150  cmpt 5233  dom cdm 5680  ran crn 5681  wf 6547  cfv 6551  (class class class)co 7424  cmpo 7426  cr 11143  1c1 11145   + caddc 11147   < clt 11284  cle 11285   / cdiv 11907  cn 12248  cz 12594  cuz 12858  +crp 13012  cli 15466  SAlgcsalg 45698  SMblFncsmblfn 46085
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-iin 5001  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-1st 7997  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-er 8729  df-pm 8852  df-en 8969  df-dom 8970  df-sdom 8971  df-sup 9471  df-inf 9472  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-n0 12509  df-z 12595  df-uz 12859  df-rp 13013  df-ioo 13366  df-ico 13368  df-fl 13795  df-seq 14005  df-exp 14065  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-clim 15470  df-rlim 15471  df-smblfn 46086
This theorem is referenced by:  smflimlem5  46165
  Copyright terms: Public domain W3C validator