smflimlem3 - Mathbox for Glauco Siliprandi

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

Theorem smflimlem3 39659

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
smflimlem3	⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌)))

Distinct variable groups: 𝐴,𝑘,𝑚,𝑠,𝑥 𝐶,𝑘,𝑚,𝑠 𝑦,𝐶 𝑖,𝐹,𝑘,𝑚,𝑛,𝑥 𝐹,𝑠,𝑖 𝑖,𝐻,𝑘,𝑚,𝑛 𝑖,𝐾,𝑘,𝑚,𝑠,𝑥 𝑦,𝐾,𝑖 𝑚,𝑀 𝑃,𝑘,𝑚,𝑠 𝑦,𝑃 𝑆,𝑘,𝑚,𝑠 𝑖,𝑋,𝑘,𝑚,𝑥 𝑖,𝑍,𝑘,𝑚,𝑛,𝑥 𝜑,𝑖,𝑘,𝑚 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑛,𝑠) 𝐴(𝑦,𝑖,𝑛) 𝐶(𝑥,𝑖,𝑛) 𝐷(𝑥,𝑦,𝑖,𝑘,𝑚,𝑛,𝑠) 𝑃(𝑥,𝑖,𝑛) 𝑆(𝑥,𝑦,𝑖,𝑛) 𝐹(𝑦) 𝐻(𝑥,𝑦,𝑠) 𝐼(𝑥,𝑦,𝑖,𝑘,𝑚,𝑛,𝑠) 𝐾(𝑛) 𝑀(𝑥,𝑦,𝑖,𝑘,𝑛,𝑠) 𝑋(𝑦,𝑛,𝑠) 𝑌(𝑥,𝑦,𝑖,𝑘,𝑚,𝑛,𝑠) 𝑍(𝑦,𝑠)

**Proof of Theorem smflimlem3**
Step	Hyp	Ref	Expression
1		smflimlem3.d	. . . . . . . . 9 ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }
2		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
3	1, 2	eqsstri 3598	. . . . . . . 8 ⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
4		inss1 3795	. . . . . . . . 9 ⊢ (𝐷 ∩ 𝐼) ⊆ 𝐷
5		smflimlem3.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐷 ∩ 𝐼))
6	4, 5	sseldi 3566	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
7	3, 6	sseldi 3566	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
8		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑚 → (𝐹‘𝑖) = (𝐹‘𝑚))
9	8	dmeqd 5248	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → dom (𝐹‘𝑖) = dom (𝐹‘𝑚))
10		eqcom 2617	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑚 ↔ 𝑚 = 𝑖)
11	10	imbi1i 338	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 𝑚 → dom (𝐹‘𝑖) = dom (𝐹‘𝑚)) ↔ (𝑚 = 𝑖 → dom (𝐹‘𝑖) = dom (𝐹‘𝑚)))
12		eqcom 2617	. . . . . . . . . . . . . 14 ⊢ (dom (𝐹‘𝑖) = dom (𝐹‘𝑚) ↔ dom (𝐹‘𝑚) = dom (𝐹‘𝑖))
13	12	imbi2i 325	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑖 → dom (𝐹‘𝑖) = dom (𝐹‘𝑚)) ↔ (𝑚 = 𝑖 → dom (𝐹‘𝑚) = dom (𝐹‘𝑖)))
14	11, 13	bitri 263	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝑚 → dom (𝐹‘𝑖) = dom (𝐹‘𝑚)) ↔ (𝑚 = 𝑖 → dom (𝐹‘𝑚) = dom (𝐹‘𝑖)))
15	9, 14	mpbi 219	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → dom (𝐹‘𝑚) = dom (𝐹‘𝑖))
16	15	cbviinv 4496	. . . . . . . . . 10 ⊢ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑖 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑖)
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑖 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑖))
18	17	iuneq2i 4475	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑖)
19		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑚))
20	19	iineq1d 38295	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → ∩ 𝑖 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑖) = ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖))
21	20	cbviunv 4495	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑖) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖)
22	18, 21	eqtri 2632	. . . . . . 7 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖)
23	7, 22	syl6eleq 2698	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖))
24		smflimlem3.z	. . . . . . . 8 ⊢ 𝑍 = (ℤ_≥‘𝑀)
25		eqid 2610	. . . . . . . 8 ⊢ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖)
26	24, 25	allbutfi 38557	. . . . . . 7 ⊢ (𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖) ↔ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ dom (𝐹‘𝑖))
27	26	biimpi 205	. . . . . 6 ⊢ (𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)dom (𝐹‘𝑖) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ dom (𝐹‘𝑖))
28	23, 27	syl 17	. . . . 5 ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ dom (𝐹‘𝑖))
29	5	elin2d 3765	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐼)
30		smflimlem3.i	. . . . . . . . 9 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘)
31		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (𝑚𝐻𝑘) = (𝑖𝐻𝑘))
32	31	cbviinv 4496	. . . . . . . . . . . . . 14 ⊢ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘) = ∩ 𝑖 ∈ (ℤ_≥‘𝑛)(𝑖𝐻𝑘)
33	32	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘) = ∩ 𝑖 ∈ (ℤ_≥‘𝑛)(𝑖𝐻𝑘))
34	33	iuneq2i 4475	. . . . . . . . . . . 12 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑛)(𝑖𝐻𝑘)
35	19	iineq1d 38295	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ∩ 𝑖 ∈ (ℤ_≥‘𝑛)(𝑖𝐻𝑘) = ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘))
36	35	cbviunv 4495	. . . . . . . . . . . 12 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑛)(𝑖𝐻𝑘) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘)
37	34, 36	eqtri 2632	. . . . . . . . . . 11 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘)
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘))
39	38	iineq2i 4476	. . . . . . . . 9 ⊢ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)(𝑚𝐻𝑘) = ∩ 𝑘 ∈ ℕ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘)
40	30, 39	eqtri 2632	. . . . . . . 8 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘)
41	29, 40	syl6eleq 2698	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘))
42		smflimlem3.k	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ)
43		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐾 → (𝑖𝐻𝑘) = (𝑖𝐻𝐾))
44	43	adantr 480	. . . . . . . . . 10 ⊢ ((𝑘 = 𝐾 ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → (𝑖𝐻𝑘) = (𝑖𝐻𝐾))
45	44	iineq2dv 4479	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘) = ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾))
46	45	iuneq2d 4483	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾))
47	46	eleq2d 2673	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝑘) ↔ 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾)))
48	41, 42, 47	eliind 38266	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾))
49		eqid 2610	. . . . . . 7 ⊢ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾)
50	24, 49	allbutfi 38557	. . . . . 6 ⊢ (𝑋 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈ (ℤ_≥‘𝑚)(𝑖𝐻𝐾) ↔ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ (𝑖𝐻𝐾))
51	48, 50	sylib 207	. . . . 5 ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ (𝑖𝐻𝐾))
52	28, 51	jca 553	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ dom (𝐹‘𝑖) ∧ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ (𝑖𝐻𝐾)))
53	24	rexanuz2 13937	. . . 4 ⊢ (∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾)) ↔ (∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ dom (𝐹‘𝑖) ∧ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)𝑋 ∈ (𝑖𝐻𝐾)))
54	52, 53	sylibr 223	. . 3 ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾)))
55		simpll 786	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → 𝜑)
56		simpr 476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍)
57	24	uztrn2 11581	. . . . . . 7 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → 𝑖 ∈ 𝑍)
58	56, 57	sylan 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → 𝑖 ∈ 𝑍)
59		simprl 790	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → 𝑋 ∈ dom (𝐹‘𝑖))
60		simp3 1056	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → 𝑋 ∈ (𝑖𝐻𝐾))
61		smflimlem3.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))
62	61	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))))
63		oveq12 6558	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → (𝑚𝑃𝑘) = (𝑖𝑃𝐾))
64	63	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → (𝐶‘(𝑚𝑃𝑘)) = (𝐶‘(𝑖𝑃𝐾)))
65	64	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑚 = 𝑖 ∧ 𝑘 = 𝐾)) → (𝐶‘(𝑚𝑃𝑘)) = (𝐶‘(𝑖𝑃𝐾)))
66		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
67	42	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐾 ∈ ℕ)
68		fvex 6113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶‘(𝑖𝑃𝐾)) ∈ V
69	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐶‘(𝑖𝑃𝐾)) ∈ V)
70	62, 65, 66, 67, 69	ovmpt2d 6686	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑖𝐻𝐾) = (𝐶‘(𝑖𝑃𝐾)))
71	70	3adant3 1074	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → (𝑖𝐻𝐾) = (𝐶‘(𝑖𝑃𝐾)))
72	60, 71	eleqtrd 2690	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → 𝑋 ∈ (𝐶‘(𝑖𝑃𝐾)))
73	72	3expa 1257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → 𝑋 ∈ (𝐶‘(𝑖𝑃𝐾)))
74	73	adantrl 748	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → 𝑋 ∈ (𝐶‘(𝑖𝑃𝐾)))
75	74, 59	elind 3760	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → 𝑋 ∈ ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖)))
76		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}
77		smflimlem3.s	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑆 ∈ SAlg)
78	76, 77	rabexd 4741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V)
79	78	ralrimivw 2950	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V)
80	79	a1d 25	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑚 ∈ 𝑍 → ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V))
81	80	imp 444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V)
82	81	ralrimiva 2949	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V)
83		smflimlem3.p	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})
84	83	fnmpt2 7127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V → 𝑃 Fn (𝑍 × ℕ))
85	82, 84	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 Fn (𝑍 × ℕ))
86	85	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑃 Fn (𝑍 × ℕ))
87		fnovrn 6707	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 Fn (𝑍 × ℕ) ∧ 𝑖 ∈ 𝑍 ∧ 𝐾 ∈ ℕ) → (𝑖𝑃𝐾) ∈ ran 𝑃)
88	86, 66, 67, 87	syl3anc 1318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑖𝑃𝐾) ∈ ran 𝑃)
89		ovex 6577	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖𝑃𝐾) ∈ V
90		eleq1 2676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑖𝑃𝐾) → (𝑦 ∈ ran 𝑃 ↔ (𝑖𝑃𝐾) ∈ ran 𝑃))
91	90	anbi2d 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑖𝑃𝐾) → ((𝜑 ∧ 𝑦 ∈ ran 𝑃) ↔ (𝜑 ∧ (𝑖𝑃𝐾) ∈ ran 𝑃)))
92		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑖𝑃𝐾) → (𝐶‘𝑦) = (𝐶‘(𝑖𝑃𝐾)))
93		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑖𝑃𝐾) → 𝑦 = (𝑖𝑃𝐾))
94	92, 93	eleq12d 2682	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑖𝑃𝐾) → ((𝐶‘𝑦) ∈ 𝑦 ↔ (𝐶‘(𝑖𝑃𝐾)) ∈ (𝑖𝑃𝐾)))
95	91, 94	imbi12d 333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑖𝑃𝐾) → (((𝜑 ∧ 𝑦 ∈ ran 𝑃) → (𝐶‘𝑦) ∈ 𝑦) ↔ ((𝜑 ∧ (𝑖𝑃𝐾) ∈ ran 𝑃) → (𝐶‘(𝑖𝑃𝐾)) ∈ (𝑖𝑃𝐾))))
96		smflimlem3.c	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → (𝐶‘𝑦) ∈ 𝑦)
97	89, 95, 96	vtocl 3232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖𝑃𝐾) ∈ ran 𝑃) → (𝐶‘(𝑖𝑃𝐾)) ∈ (𝑖𝑃𝐾))
98	88, 97	syldan 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐶‘(𝑖𝑃𝐾)) ∈ (𝑖𝑃𝐾))
99	83	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}))
100	15	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → dom (𝐹‘𝑚) = dom (𝐹‘𝑖))
101	8	fveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑚 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥))
102	10	imbi1i 338	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑖 = 𝑚 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) ↔ (𝑚 = 𝑖 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥)))
103		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥) ↔ ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑖)‘𝑥))
104	103	imbi2i 325	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 = 𝑖 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) ↔ (𝑚 = 𝑖 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑖)‘𝑥)))
105	102, 104	bitri 263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 = 𝑚 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) ↔ (𝑚 = 𝑖 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑖)‘𝑥)))
106	101, 105	mpbi 219	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑖)‘𝑥))
107	106	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑖)‘𝑥))
108		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → (1 / 𝑘) = (1 / 𝐾))
109	108	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → (𝐴 + (1 / 𝑘)) = (𝐴 + (1 / 𝐾)))
110	109	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → (𝐴 + (1 / 𝑘)) = (𝐴 + (1 / 𝐾)))
111	107, 110	breq12d 4596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → (((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))))
112	100, 111	rabeqbidv 3168	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))})
113	15	ineq2d 3776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑖 → (𝑠 ∩ dom (𝐹‘𝑚)) = (𝑠 ∩ dom (𝐹‘𝑖)))
114	113	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → (𝑠 ∩ dom (𝐹‘𝑚)) = (𝑠 ∩ dom (𝐹‘𝑖)))
115	112, 114	eqeq12d 2625	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)) ↔ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))))
116	115	rabbidv 3164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑖 ∧ 𝑘 = 𝐾) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))})
117	116	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑚 = 𝑖 ∧ 𝑘 = 𝐾)) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))})
118		eqid 2610	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))}
119	118, 77	rabexd 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))} ∈ V)
120	119	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))} ∈ V)
121	99, 117, 66, 67, 120	ovmpt2d 6686	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑖𝑃𝐾) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))})
122	98, 121	eleqtrd 2690	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐶‘(𝑖𝑃𝐾)) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))})
123		ineq1 3769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐶‘(𝑖𝑃𝐾)) → (𝑠 ∩ dom (𝐹‘𝑖)) = ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖)))
124	123	eqeq2d 2620	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐶‘(𝑖𝑃𝐾)) → ({𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖)) ↔ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖))))
125	124	elrab 3331	. . . . . . . . . . . . . . 15 ⊢ ((𝐶‘(𝑖𝑃𝐾)) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = (𝑠 ∩ dom (𝐹‘𝑖))} ↔ ((𝐶‘(𝑖𝑃𝐾)) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖))))
126	122, 125	sylib 207	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝐶‘(𝑖𝑃𝐾)) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖))))
127	126	simprd 478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} = ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖)))
128	127	eqcomd 2616	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖)) = {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))})
129	128	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → ((𝐶‘(𝑖𝑃𝐾)) ∩ dom (𝐹‘𝑖)) = {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))})
130	75, 129	eleqtrd 2690	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → 𝑋 ∈ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))})
131		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑖)‘𝑋))
132		eqidd 2611	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝐴 + (1 / 𝐾)) = (𝐴 + (1 / 𝐾)))
133	131, 132	breq12d 4596	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾)) ↔ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))))
134	133	elrab 3331	. . . . . . . . . 10 ⊢ (𝑋 ∈ {𝑥 ∈ dom (𝐹‘𝑖) ∣ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (1 / 𝐾))} ↔ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))))
135	130, 134	sylib 207	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))))
136	135	simprd 478	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))
137	59, 136	jca 553	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾))) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))))
138	137	ex 449	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))))
139	55, 58, 138	syl2anc 691	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → ((𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))))
140	139	ralimdva 2945	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))))
141	140	reximdva 3000	. . 3 ⊢ (𝜑 → (∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ 𝑋 ∈ (𝑖𝐻𝐾)) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))))
142	54, 141	mpd 15	. 2 ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))))
143		simprl 790	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → 𝑋 ∈ dom (𝐹‘𝑖))
144		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑚((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ)
145		eleq1 2676	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (𝑚 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍))
146	145	anbi2d 736	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍)))
147		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖))
148	147, 15	feq12d 5946	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ ↔ (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ))
149	146, 148	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ)))
150	77	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg)
151		smflimlem3.m	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆))
152		eqid 2610	. . . . . . . . . . . . 13 ⊢ dom (𝐹‘𝑚) = dom (𝐹‘𝑚)
153	150, 151, 152	smff 39618	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)
154	144, 149, 153	chvar 2250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ)
155	154	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑋 ∈ dom (𝐹‘𝑖)) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ)
156		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑋 ∈ dom (𝐹‘𝑖)) → 𝑋 ∈ dom (𝐹‘𝑖))
157	155, 156	ffvelrnd 6268	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑋 ∈ dom (𝐹‘𝑖)) → ((𝐹‘𝑖)‘𝑋) ∈ ℝ)
158	157	adantrr 749	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → ((𝐹‘𝑖)‘𝑋) ∈ ℝ)
159		smflimlem3.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℝ)
160	42	nnrecred 10943	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝐾) ∈ ℝ)
161	159, 160	readdcld 9948	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + (1 / 𝐾)) ∈ ℝ)
162	161	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → (𝐴 + (1 / 𝐾)) ∈ ℝ)
163		smflimlem3.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ ℝ⁺)
164	163	rpred 11748	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
165	159, 164	readdcld 9948	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + 𝑌) ∈ ℝ)
166	165	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → (𝐴 + 𝑌) ∈ ℝ)
167		simprr 792	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))
168		smflimlem3.l	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝐾) < 𝑌)
169	160, 164, 159, 168	ltadd2dd 10075	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + (1 / 𝐾)) < (𝐴 + 𝑌))
170	169	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → (𝐴 + (1 / 𝐾)) < (𝐴 + 𝑌))
171	158, 162, 166, 167, 170	lttrd 10077	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌))
172	143, 171	jca 553	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾)))) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌)))
173	172	ex 449	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌))))
174	55, 58, 173	syl2anc 691	. . . 4 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → ((𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))) → (𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌))))
175	174	ralimdva 2945	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))) → ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌))))
176	175	reximdva 3000	. 2 ⊢ (𝜑 → (∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + (1 / 𝐾))) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌))))
177	142, 176	mpd 15	1 ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 {crab 2900 Vcvv 3173 ∩ cin 3539 ∪ ciun 4455 ∩ ciin 4456 class class class wbr 4583 ↦ cmpt 4643 × cxp 5036 dom cdm 5038 ran crn 5039 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 ℝcr 9814 1c1 9816 + caddc 9818 < clt 9953 / cdiv 10563 ℕcn 10897 ℤ_≥cuz 11563 ℝ⁺crp 11708 ⇝ cli 14063 SAlgcsalg 39204 SMblFncsmblfn 39586

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-z 11255 df-uz 11564 df-rp 11709 df-ioo 12050 df-ico 12052 df-smblfn 39587

This theorem is referenced by: smflimlem4 39660

W3C validator