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