Metamath Proof Explorer

Theorem subsaliuncl

Description: A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of Fremlin1 p. 35. 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 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 omelon ⊢ ω ∈ On
12 nnct ⊢ ℕ ≼ ω
13 ondomen ⊢ ( ( ω ∈ On ∧ ℕ ≼ ω ) → ℕ ∈ dom card )
14 11 12 13 mp2an ⊢ ℕ ∈ dom card
15 fnrndomnum ⊢ ( ℕ ∈ dom card → ( ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) Fn ℕ → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ ) )
16 14 15 ax-mp ⊢ ( ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) Fn ℕ → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ )
17 10 16 syl ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ )
18 12 a1i ⊢ ( 𝜑 → ℕ ≼ ω )
19 domtr ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ℕ ∧ ℕ ≼ ω ) → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ω )
20 17 18 19 syl2anc ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ≼ ω )
21 vex ⊢ 𝑦 ∈ V
22 8 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
23 21 22 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
24 23 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
25 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
26 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )
27 26 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) )
28 2 elexd ⊢ ( 𝜑 → 𝐷 ∈ V )
29 elrest ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐷 ∈ V ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ) )
30 1 28 29 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ) )
32 27 31 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) )
33 rabn0 ⊢ ( { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) )
34 32 33 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ≠ ∅ )
35 34 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ≠ ∅ )
36 25 35 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑦 ≠ ∅ )
37 36 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ → ( 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ≠ ∅ ) ) )
38 37 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ≠ ∅ ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ) → ( ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ≠ ∅ ) )
40 24 39 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ) → 𝑦 ≠ ∅ )
41 20 40 axccdom ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
42 simpl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝜑 )
43 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
44 43 eqeq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ↔ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) ) )
45 44 rabbidv ⊢ ( 𝑛 = 𝑚 → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } )
46 45 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } )
47 46 rneqi ⊢ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } )
48 47 fneq2i ⊢ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ↔ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) )
49 48 biimpi ⊢ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) )
50 49 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) )
51 47 raleqi ⊢ ( ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
52 51 bilani ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 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 46 59 eqtr2i ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑧 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) } ) = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
61 60 coeq2i ⊢ ( 𝑓 ∘ ( 𝑚 ∈ ℕ ↦ { 𝑧 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑧 ∩ 𝐷 ) } ) ) = ( 𝑓 ∘ ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
62 48 biimpri ⊢ ( 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) → 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
63 62 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 Fn ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
64 47 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 42 50 53 73 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
75 74 ex ⊢ ( 𝜑 → ( ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) )
76 75 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 Fn ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ∧ ∀ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) )
77 41 76 mpd ⊢ ( 𝜑 → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
78 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑆 ∈ SAlg )
79 28 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝐷 ∈ V )
80 1 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → 𝑆 ∈ SAlg )
81 12 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → ℕ ≼ ω )
82 elmapi ⊢ ( 𝑒 ∈ ( 𝑆 ↑m ℕ ) → 𝑒 : ℕ ⟶ 𝑆 )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → 𝑒 : ℕ ⟶ 𝑆 )
84 83 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
85 80 81 84 saliuncl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
86 85 3adant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
87 eqid ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 )
88 78 79 86 87 elrestd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) )
89 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 )
90 rspa ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
91 89 90 iuneq2df ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
92 iunin1 ⊢ ∪ 𝑛 ∈ ℕ ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 )
93 92 a1i ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
94 91 93 eqtrd ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
95 94 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
96 3 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → 𝑇 = ( 𝑆 ↾t 𝐷 ) )
97 95 96 eleq12d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ( ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 ↔ ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
98 88 97 mpbird ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )
99 98 3exp ⊢ ( 𝜑 → ( 𝑒 ∈ ( 𝑆 ↑m ℕ ) → ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 ) ) )
100 99 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 ) )
101 77 100 mpd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑇 )