Theorem smflimlem6

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 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	smflimlem6.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smflimlem6.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smflimlem6.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smflimlem6.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smflimlem6.5	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
	smflimlem6.6	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
	smflimlem6.7	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	smflimlem6.8	⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
Assertion	smflimlem6	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smflimlem6.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		smflimlem6.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		smflimlem6.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smflimlem6.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5		smflimlem6.5	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
6		smflimlem6.6	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
7		smflimlem6.7	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
8		smflimlem6.8	⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
9	2	fvexi	⊢ 𝑍 ∈ V
10		nnex	⊢ ℕ ∈ V
11	9 10	xpex	⊢ ( 𝑍 × ℕ ) ∈ V
12	11	a1i	⊢ ( 𝜑 → ( 𝑍 × ℕ ) ∈ V )
13		eqid	⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
14	13 3	rabexd	⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
16	15	ralrimivva	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
17	8	fnmpo	⊢ ( ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V → 𝑃 Fn ( 𝑍 × ℕ ) )
18	16 17	syl	⊢ ( 𝜑 → 𝑃 Fn ( 𝑍 × ℕ ) )
19		fnrndomg	⊢ ( ( 𝑍 × ℕ ) ∈ V → ( 𝑃 Fn ( 𝑍 × ℕ ) → ran 𝑃 ≼ ( 𝑍 × ℕ ) ) )
20	12 18 19	sylc	⊢ ( 𝜑 → ran 𝑃 ≼ ( 𝑍 × ℕ ) )
21	2	uzct	⊢ 𝑍 ≼ ω
22		nnct	⊢ ℕ ≼ ω
23	21 22	pm3.2i	⊢ ( 𝑍 ≼ ω ∧ ℕ ≼ ω )
24		xpct	⊢ ( ( 𝑍 ≼ ω ∧ ℕ ≼ ω ) → ( 𝑍 × ℕ ) ≼ ω )
25	23 24	ax-mp	⊢ ( 𝑍 × ℕ ) ≼ ω
26	25	a1i	⊢ ( 𝜑 → ( 𝑍 × ℕ ) ≼ ω )
27		domtr	⊢ ( ( ran 𝑃 ≼ ( 𝑍 × ℕ ) ∧ ( 𝑍 × ℕ ) ≼ ω ) → ran 𝑃 ≼ ω )
28	20 26 27	syl2anc	⊢ ( 𝜑 → ran 𝑃 ≼ ω )
29		vex	⊢ 𝑦 ∈ V
30	8	elrnmpog	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran 𝑃 ↔ ∃ 𝑚 ∈ 𝑍 ∃ 𝑘 ∈ ℕ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
31	29 30	ax-mp	⊢ ( 𝑦 ∈ ran 𝑃 ↔ ∃ 𝑚 ∈ 𝑍 ∃ 𝑘 ∈ ℕ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
32	31	biimpi	⊢ ( 𝑦 ∈ ran 𝑃 → ∃ 𝑚 ∈ 𝑍 ∃ 𝑘 ∈ ℕ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → ∃ 𝑚 ∈ 𝑍 ∃ 𝑘 ∈ ℕ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
34		simp3	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
35	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → 𝑆 ∈ SAlg )
36	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
37	36	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
38		eqid	⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
39	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ )
40		nnrecre	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
41	40	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ )
42	39 41	readdcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 + ( 1 / 𝑘 ) ) ∈ ℝ )
43	42	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → ( 𝐴 + ( 1 / 𝑘 ) ) ∈ ℝ )
44	35 37 38 43	smfpreimalt	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) )
45		fvex	⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
46	45	dmex	⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
47	46	a1i	⊢ ( 𝜑 → dom ( 𝐹 ‘ 𝑚 ) ∈ V )
48		elrest	⊢ ( ( 𝑆 ∈ SAlg ∧ dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
49	3 47 48	syl2anc	⊢ ( 𝜑 → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
50	49	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
51	44 50	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → ∃ 𝑠 ∈ 𝑆 { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
52		rabn0	⊢ ( { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ ↔ ∃ 𝑠 ∈ 𝑆 { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
53	51 52	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ )
54	53	3adant3	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ )
55	34 54	eqnetrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → 𝑦 ≠ ∅ )
56	55	3exp	⊢ ( 𝜑 → ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ) → ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) ) )
57	56	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑍 ∃ 𝑘 ∈ ℕ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) )
58	57	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → ( ∃ 𝑚 ∈ 𝑍 ∃ 𝑘 ∈ ℕ 𝑦 = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) )
59	33 58	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → 𝑦 ≠ ∅ )
60	28 59	axccd2	⊢ ( 𝜑 → ∃ 𝑐 ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 )
61	1	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑀 ∈ ℤ )
62	3	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑆 ∈ SAlg )
63	4	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
64	7	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ ℝ )
65		fvoveq1	⊢ ( 𝑙 = 𝑚 → ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) = ( 𝑐 ‘ ( 𝑚 𝑃 𝑗 ) ) )
66		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑚 𝑃 𝑗 ) = ( 𝑚 𝑃 𝑘 ) )
67	66	fveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑐 ‘ ( 𝑚 𝑃 𝑗 ) ) = ( 𝑐 ‘ ( 𝑚 𝑃 𝑘 ) ) )
68	65 67	cbvmpov	⊢ ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑚 𝑃 𝑘 ) ) )
69		nfcv	⊢ Ⅎ 𝑘 ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 )
70		nfcv	⊢ Ⅎ 𝑗 𝑍
71		nfcv	⊢ Ⅎ 𝑗 ( ℤ≥ ‘ 𝑛 )
72		nfcv	⊢ Ⅎ 𝑗 𝑚
73		nfmpo2	⊢ Ⅎ 𝑗 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) )
74		nfcv	⊢ Ⅎ 𝑗 𝑘
75	72 73 74	nfov	⊢ Ⅎ 𝑗 ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 )
76	71 75	nfiin	⊢ Ⅎ 𝑗 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 )
77	70 76	nfiun	⊢ Ⅎ 𝑗 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 )
78		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
79	78	adantr	⊢ ( ( 𝑗 = 𝑘 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
80	79	iineq2dv	⊢ ( 𝑗 = 𝑘 → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
81		oveq1	⊢ ( 𝑖 = 𝑚 → ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) = ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
82	81	cbviinv	⊢ ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 )
83	82	a1i	⊢ ( 𝑗 = 𝑘 → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
84	80 83	eqtrd	⊢ ( 𝑗 = 𝑘 → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
85	84	adantr	⊢ ( ( 𝑗 = 𝑘 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
86	85	iuneq2dv	⊢ ( 𝑗 = 𝑘 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 ) )
87	69 77 86	cbviin	⊢ ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑖 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑗 ) = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ ( 𝑐 ‘ ( 𝑙 𝑃 𝑗 ) ) ) 𝑘 )
88		fveq2	⊢ ( 𝑦 = 𝑟 → ( 𝑐 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑟 ) )
89		id	⊢ ( 𝑦 = 𝑟 → 𝑦 = 𝑟 )
90	88 89	eleq12d	⊢ ( 𝑦 = 𝑟 → ( ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑐 ‘ 𝑟 ) ∈ 𝑟 ) )
91	90	rspccva	⊢ ( ( ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝑐 ‘ 𝑟 ) ∈ 𝑟 )
92	91	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝑐 ‘ 𝑟 ) ∈ 𝑟 )
93	61 2 62 63 5 6 64 8 68 87 92	smflimlem5	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
94	93	ex	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
95	94	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑐 ∀ 𝑦 ∈ ran 𝑃 ( 𝑐 ‘ 𝑦 ) ∈ 𝑦 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
96	60 95	mpd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )