Metamath Proof Explorer

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 . The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Vincent Gonzalez, 30-Aug-2026)

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