Theorem smflimlem2

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	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	smflimlem2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷 ∩ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		smflimlem2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		smflimlem2.2	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smflimlem2.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
4		smflimlem2.4	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
5		smflimlem2.5	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
6		smflimlem2.6	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7		smflimlem2.7	⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
8		smflimlem2.8	⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
9		smflimlem2.9	⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
10		smflimlem2.10	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
11		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
12	4 11	nfcxfr	⊢ Ⅎ 𝑥 𝐷
13	12	ssrab2f	⊢ { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐷
14	13	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐷 )
15		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ 𝐷 )
16		ssrab2	⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
17	4 16	eqsstri	⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
18	17	sseli	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
19		fveq2	⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) )
20	19	iineq1d	⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
21	20	cbviunv	⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
22	21	eleq2i	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
23		eliun	⊢ ( 𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
24	22 23	bitri	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
25	18 24	sylib	⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
26	15 25	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
27		nfv	⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
28		nfv	⊢ Ⅎ 𝑚 𝑘 ∈ ℕ
29	27 28	nfan	⊢ Ⅎ 𝑚 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ )
30		nfv	⊢ Ⅎ 𝑚 𝑖 ∈ 𝑍
31	29 30	nfan	⊢ Ⅎ 𝑚 ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 )
32		nfcv	⊢ Ⅎ 𝑚 𝑥
33		nfii1	⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
34	32 33	nfel	⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 )
35	31 34	nfan	⊢ Ⅎ 𝑚 ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
36		nfmpt1	⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
37		eqid	⊢ ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑖 )
38		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
39	1	eleq2i	⊢ ( 𝑖 ∈ 𝑍 ↔ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
40	39	biimpi	⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
41	38 40	sselid	⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ℤ )
42		uzid	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) )
43	41 42	syl	⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) )
44	43	ad2antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) )
45		simplll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) )
46	45	simpld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 )
47		uzss	⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
48	40 47	syl	⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
49	48 1	sseqtrrdi	⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 )
50	49	sselda	⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑚 ∈ 𝑍 )
51	50	ad4ant24	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑚 ∈ 𝑍 )
52		eliinid	⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
53	52	adantll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
54		eqidd	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
55		fvexd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
56	54 55	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
57	56	3adant3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
58	2	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
59	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
60		eqid	⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
61	58 59 60	smff	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
62	61	3adant3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
63		simp3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
64	62 63	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
65	57 64	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
66	46 51 53 65	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
67	66	adantl3r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
68	67	adantl3r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ )
69	4	eleq2i	⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
70	69	biimpi	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
71		rabidim2	⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
72	70 71	syl	⊢ ( 𝑥 ∈ 𝐷 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
73		climdm	⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
74	72 73	sylib	⊢ ( 𝑥 ∈ 𝐷 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
75	74	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
76	75 73	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
77	76 73	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
78		nfcv	⊢ Ⅎ 𝑥 𝐹
79		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
80	12 78 5 79	fnlimfv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
81	80	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝑥 ) )
82	77 81	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
83	82	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
84	6	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝐴 ∈ ℝ )
85		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 )
86		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
87		nnrecrp	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
88	86 87	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 1 / 𝑘 ) ∈ ℝ+ )
89	35 36 37 44 68 83 84 85 88	climleltrp	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
90		simp-6l	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 )
91		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑖 ∈ 𝑍 )
92	91	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑖 ∈ 𝑍 )
93		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
94		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) )
95		nfv	⊢ Ⅎ 𝑚 𝜑
96	95 30 34	nf3an	⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) )
97		nfv	⊢ Ⅎ 𝑚 𝑛 ∈ ( ℤ≥ ‘ 𝑖 )
98	96 97	nfan	⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) )
99		simpll	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) )
100	37	uztrn2	⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) )
101	100	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) )
102		simpll2	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑖 ∈ 𝑍 )
103		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) )
104	102 103 50	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑚 ∈ 𝑍 )
105		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
106		id	⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍 )
107		fvexd	⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
108		eqid	⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
109	108	fvmpt2	⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
110	106 107 109	syl2anc	⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
111	110	eqcomd	⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) )
112	111	adantr	⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) )
113		simpr	⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
114	112 113	eqbrtrd	⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
115	104 105 114	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
116	52	3ad2antl3	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
117	116	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
118		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) )
119	117 118	jca	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
120		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
121	119 120	sylibr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
122	115 121	syldan	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
123	122	adantrl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
124	123	ex	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
125	99 101 124	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
126	98 125	ralimdaa	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
127	90 92 93 94 126	syl31anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
128	127	reximdva	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
129	89 128	mpd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
130		ssrexv	⊢ ( ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
131	49 130	syl	⊢ ( 𝑖 ∈ 𝑍 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
132	131	ad2antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
133	129 132	mpd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
134	133	rexlimdva2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) )
135	26 134	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
136		nfv	⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 )
137		nfra1	⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) }
138	136 137	nfan	⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
139		simpll1	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
140		simpll2	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
141	1	uztrn2	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 )
142	141	ssd	⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
143	142	sselda	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
144	143	adantll	⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
145	144	3adantl1	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
146	145	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
147		rspa	⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
148	147	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
149		simp1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝜑 )
150		simp3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
151		simp2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑘 ∈ ℕ )
152		eqid	⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
153	152 2	rabexd	⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
154	153	ralrimivw	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
155	154	ralrimivw	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
156	155	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
157	7	elrnmpoid	⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 )
158	150 151 156 157	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 )
159		ovex	⊢ ( 𝑚 𝑃 𝑘 ) ∈ V
160		eleq1	⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝑟 ∈ ran 𝑃 ↔ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) )
161	160	anbi2d	⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) ↔ ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) ) )
162		fveq2	⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝐶 ‘ 𝑟 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
163		id	⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → 𝑟 = ( 𝑚 𝑃 𝑘 ) )
164	162 163	eleq12d	⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ↔ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) )
165	161 164	imbi12d	⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) ↔ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) ) )
166	159 165 10	vtocl	⊢ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) )
167	149 158 166	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) )
168		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V )
169	8	ovmpt4g	⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
170	150 151 168 169	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
171	170	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝑚 𝐻 𝑘 ) )
172	149 153	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
173	7	ovmpt4g	⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
174	150 151 172 173	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
175	171 174	eleq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ↔ ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
176	167 175	mpbid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
177		ineq1	⊢ ( 𝑠 = ( 𝑚 𝐻 𝑘 ) → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
178	177	eqeq2d	⊢ ( 𝑠 = ( 𝑚 𝐻 𝑘 ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
179	178	elrab	⊢ ( ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ↔ ( ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
180	176 179	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
181	180	simprd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
182		inss1	⊢ ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝑚 𝐻 𝑘 )
183	181 182	eqsstrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ⊆ ( 𝑚 𝐻 𝑘 ) )
184	183	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ⊆ ( 𝑚 𝐻 𝑘 ) )
185		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
186	184 185	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
187	139 140 146 148 186	syl31anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
188	187	ex	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) )
189	138 188	ralrimi	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
190		vex	⊢ 𝑥 ∈ V
191		eliin	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) )
192	190 191	ax-mp	⊢ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) )
193	189 192	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
194	193	ex	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
195	194	ad5ant145	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
196	195	reximdva	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
197	135 196	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
198		eliun	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
199	197 198	sylibr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
200	199	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
201		eliin	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) )
202	190 201	ax-mp	⊢ ( 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
203	200 202	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) )
204	203 9	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → 𝑥 ∈ 𝐼 )
205	204	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) )
206	205	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) )
207		rabss	⊢ ( { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) )
208	206 207	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐼 )
209	14 208	ssind	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷 ∩ 𝐼 ) )