Metamath Proof Explorer

Theorem subsaliuncl

Description: A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of Fremlin1 p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses subsaliuncl.1 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
subsaliuncl.2 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
subsaliuncl.3 ⊢ 𝑇 = ( 𝑆 ↾t 𝐷 )
subsaliuncl.4 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑇 )
Assertion subsaliuncl ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 subsaliuncl.1 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 subsaliuncl.2 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 subsaliuncl.3 ⊢ 𝑇 = ( 𝑆 ↾t 𝐷 )
4 subsaliuncl.4 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑇 )
5 eqid ⊢ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) }
6 5 1 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V )
7 6 ralrimivw ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V )
8 eqid ⊢ ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
9 8 fnmpt ⊢ ( ∀ 𝑛 ∈ ℕ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V → ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) Fn ℕ )
10 7 9 syl ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) Fn ℕ )
11 nnex ⊢ ℕ ∈ V
12 fnrndomg ⊢ ( ℕ ∈ V → ( ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) Fn ℕ → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ ) )
13 11 12 ax-mp ⊢ ( ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) Fn ℕ → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ )
14 10 13 syl ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ )
15 nnenom ⊢ ℕ ≈ ω
16 15 a1i ⊢ ( 𝜑 → ℕ ≈ ω )
17 domentr ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ ∧ ℕ ≈ ω ) → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ω )
18 14 16 17 syl2anc ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ω )
19 vex ⊢ 𝑦 ∈ V
20 8 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
21 19 20 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
22 21 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
23 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
24 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )
25 24 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) )
26 2 elexd ⊢ ( 𝜑 → 𝐷 ∈ V )
27 elrest ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐷 ∈ V ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ) )
28 1 26 27 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ) )
30 25 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) )
31 rabn0 ⊢ ( { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) )
32 30 31 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ≠ ∅ )
33 32 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ≠ ∅ )
34 23 33 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑦 ≠ ∅ )
35 34 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ → ( 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ≠ ∅ ) ) )
36 35 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ≠ ∅ ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ) → ( ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ≠ ∅ ) )
38 22 37 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ) → 𝑦 ≠ ∅ )
39 18 38 axccdom ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
40 simpl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝜑 )
41 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
42 41 eqeq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ↔ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) ) )
43 42 rabbidv ⊢ ( 𝑛 = 𝑚 → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } )
44 43 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } )
45 44 rneqi ⊢ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } )
46 45 fneq2i ⊢ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ↔ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) )
47 46 biimpi ⊢ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) )
48 47 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) )
49 45 raleqi ⊢ ( ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
50 49 bilani ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
51 50 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
52 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
53 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑆 ∈ SAlg )
54 ineq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∩ 𝐷 ) = ( 𝑧 ∩ 𝐷 ) )
55 54 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) ↔ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) ) )
56 55 cbvrabv ⊢ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } = { 𝑧 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) }
57 56 mpteq2i ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑧 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) } )
58 44 57 eqtr2i ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑧 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) } ) = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
59 58 coeq2i ⊢ ( 𝑓 ∘ ( 𝑚 ∈ ℕ ↦ { 𝑧 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) } ) ) = ( 𝑓 ∘ ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
60 46 biimpri ⊢ ( 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
61 60 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
62 45 eqcomi ⊢ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) = ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
63 62 raleqi ⊢ ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
64 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) )
65 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
66 64 65 eleq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
67 66 cbvralvw ⊢ ( ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )
68 63 67 bitri ⊢ ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )
69 68 biimpi ⊢ ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )
70 69 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )
71 52 53 8 59 61 70 subsaliuncllem ⊢ ( ( 𝜑 ∧ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
72 40 48 51 71 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
73 72 ex ⊢ ( 𝜑 → ( ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) )
74 73 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) )
75 39 74 mpd ⊢ ( 𝜑 → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
76 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑆 ∈ SAlg )
77 26 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝐷 ∈ V )
78 1 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → 𝑆 ∈ SAlg )
79 nnct ⊢ ℕ ≼ ω
80 79 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → ℕ ≼ ω )
81 elmapi ⊢ ( 𝑒 ∈ ( 𝑆 ↑m ℕ ) → 𝑒 : ℕ ⟶ 𝑆 )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → 𝑒 : ℕ ⟶ 𝑆 )
83 82 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
84 78 80 83 saliuncl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
85 84 3adant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
86 eqid ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 )
87 76 77 85 86 elrestd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) )
88 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 )
89 rspa ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
90 88 89 iuneq2df ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
91 iunin1 ⊢ ∪ 𝑛 ∈ ℕ ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 )
92 91 a1i ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
93 90 92 eqtrd ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
94 93 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
95 3 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑇 = ( 𝑆 ↾t 𝐷 ) )
96 94 95 eleq12d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 ↔ ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
97 87 96 mpbird ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )
98 97 3exp ⊢ ( 𝜑 → ( 𝑒 ∈ ( 𝑆 ↑m ℕ ) → ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 ) ) )
99 98 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 ) )
100 75 99 mpd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )