# 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 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
subsaliuncl.2 ${⊢}{\phi }\to {D}\in {V}$
subsaliuncl.3 ${⊢}{T}={S}{↾}_{𝑡}{D}$
subsaliuncl.4 ${⊢}{\phi }\to {F}:ℕ⟶{T}$
Assertion subsaliuncl ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)\in {T}$

### Proof

Step Hyp Ref Expression
1 subsaliuncl.1 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
2 subsaliuncl.2 ${⊢}{\phi }\to {D}\in {V}$
3 subsaliuncl.3 ${⊢}{T}={S}{↾}_{𝑡}{D}$
4 subsaliuncl.4 ${⊢}{\phi }\to {F}:ℕ⟶{T}$
5 eqid ${⊢}\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}$
6 5 1 rabexd ${⊢}{\phi }\to \left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\in \mathrm{V}$
7 6 ralrimivw ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\in \mathrm{V}$
8 eqid ${⊢}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)=\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
9 8 fnmpt ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\in \mathrm{V}\to \left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)Fnℕ$
10 7 9 syl ${⊢}{\phi }\to \left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)Fnℕ$
11 nnex ${⊢}ℕ\in \mathrm{V}$
12 fnrndomg ${⊢}ℕ\in \mathrm{V}\to \left(\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)Fnℕ\to \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\preccurlyeq ℕ\right)$
13 11 12 ax-mp ${⊢}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)Fnℕ\to \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\preccurlyeq ℕ$
14 10 13 syl ${⊢}{\phi }\to \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\preccurlyeq ℕ$
15 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
16 15 a1i ${⊢}{\phi }\to ℕ\approx \mathrm{\omega }$
17 domentr ${⊢}\left(\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\preccurlyeq ℕ\wedge ℕ\approx \mathrm{\omega }\right)\to \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\preccurlyeq \mathrm{\omega }$
18 14 16 17 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\preccurlyeq \mathrm{\omega }$
19 vex ${⊢}{y}\in \mathrm{V}$
20 8 elrnmpt ${⊢}{y}\in \mathrm{V}\to \left({y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
21 19 20 ax-mp ${⊢}{y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}$
22 21 biimpi ${⊢}{y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}$
23 22 adantl ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}$
24 simp3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\to {y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}$
25 4 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in {T}$
26 25 3 eleqtrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \left({S}{↾}_{𝑡}{D}\right)$
27 2 elexd ${⊢}{\phi }\to {D}\in \mathrm{V}$
28 elrest ${⊢}\left({S}\in \mathrm{SAlg}\wedge {D}\in \mathrm{V}\right)\to \left({F}\left({n}\right)\in \left({S}{↾}_{𝑡}{D}\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={x}\cap {D}\right)$
29 1 27 28 syl2anc ${⊢}{\phi }\to \left({F}\left({n}\right)\in \left({S}{↾}_{𝑡}{D}\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={x}\cap {D}\right)$
30 29 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({F}\left({n}\right)\in \left({S}{↾}_{𝑡}{D}\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={x}\cap {D}\right)$
31 26 30 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={x}\cap {D}$
32 rabn0 ${⊢}\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\ne \varnothing ↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={x}\cap {D}$
33 31 32 sylibr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\ne \varnothing$
34 33 3adant3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\to \left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\ne \varnothing$
35 24 34 eqnetrd ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\to {y}\ne \varnothing$
36 35 3exp ${⊢}{\phi }\to \left({n}\in ℕ\to \left({y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\to {y}\ne \varnothing \right)\right)$
37 36 rexlimdv ${⊢}{\phi }\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\to {y}\ne \varnothing \right)$
38 37 adantr ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\to {y}\ne \varnothing \right)$
39 23 38 mpd ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\right)\to {y}\ne \varnothing$
40 18 39 axccdom ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)$
41 simpl ${⊢}\left({\phi }\wedge \left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\right)\to {\phi }$
42 fveq2 ${⊢}{n}={m}\to {F}\left({n}\right)={F}\left({m}\right)$
43 42 eqeq1d ${⊢}{n}={m}\to \left({F}\left({n}\right)={x}\cap {D}↔{F}\left({m}\right)={x}\cap {D}\right)$
44 43 rabbidv ${⊢}{n}={m}\to \left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}=\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}$
45 44 cbvmptv ${⊢}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)=\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)$
46 45 rneqi ${⊢}\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)=\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)$
47 46 fneq2i ${⊢}{f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)↔{f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)$
48 47 biimpi ${⊢}{f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\to {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)$
49 48 ad2antrl ${⊢}\left({\phi }\wedge \left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\right)\to {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)$
50 46 raleqi ${⊢}\forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}↔\forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}$
51 50 biimpi ${⊢}\forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\to \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}$
52 51 adantl ${⊢}\left({\phi }\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}$
53 52 adantrl ${⊢}\left({\phi }\wedge \left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\right)\to \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}$
54 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)$
55 1 3ad2ant1 ${⊢}\left({\phi }\wedge {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to {S}\in \mathrm{SAlg}$
56 ineq1 ${⊢}{x}={z}\to {x}\cap {D}={z}\cap {D}$
57 56 eqeq2d ${⊢}{x}={z}\to \left({F}\left({m}\right)={x}\cap {D}↔{F}\left({m}\right)={z}\cap {D}\right)$
58 57 cbvrabv ${⊢}\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}=\left\{{z}\in {S}|{F}\left({m}\right)={z}\cap {D}\right\}$
59 58 mpteq2i ${⊢}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)=\left({m}\in ℕ⟼\left\{{z}\in {S}|{F}\left({m}\right)={z}\cap {D}\right\}\right)$
60 45 59 eqtr2i ${⊢}\left({m}\in ℕ⟼\left\{{z}\in {S}|{F}\left({m}\right)={z}\cap {D}\right\}\right)=\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
61 60 coeq2i ${⊢}{f}\circ \left({m}\in ℕ⟼\left\{{z}\in {S}|{F}\left({m}\right)={z}\cap {D}\right\}\right)={f}\circ \left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
62 47 biimpri ${⊢}{f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\to {f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
63 62 3ad2ant2 ${⊢}\left({\phi }\wedge {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to {f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
64 46 eqcomi ${⊢}\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)=\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)$
65 64 raleqi ${⊢}\forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}↔\forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}$
66 fveq2 ${⊢}{y}={z}\to {f}\left({y}\right)={f}\left({z}\right)$
67 id ${⊢}{y}={z}\to {y}={z}$
68 66 67 eleq12d ${⊢}{y}={z}\to \left({f}\left({y}\right)\in {y}↔{f}\left({z}\right)\in {z}\right)$
69 68 cbvralvw ${⊢}\forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}↔\forall {z}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}$
70 65 69 bitri ${⊢}\forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}↔\forall {z}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}$
71 70 biimpi ${⊢}\forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\to \forall {z}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}$
72 71 3ad2ant3 ${⊢}\left({\phi }\wedge {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to \forall {z}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}$
73 54 55 8 61 63 72 subsaliuncllem ${⊢}\left({\phi }\wedge {f}Fn\mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({m}\in ℕ⟼\left\{{x}\in {S}|{F}\left({m}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to \exists {e}\in \left({{S}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}$
74 41 49 53 73 syl3anc ${⊢}\left({\phi }\wedge \left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\right)\to \exists {e}\in \left({{S}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}$
75 74 ex ${⊢}{\phi }\to \left(\left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to \exists {e}\in \left({{S}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)$
76 75 exlimdv ${⊢}{\phi }\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn\mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\wedge \forall {y}\in \mathrm{ran}\left({n}\in ℕ⟼\left\{{x}\in {S}|{F}\left({n}\right)={x}\cap {D}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {y}\right)\to \exists {e}\in \left({{S}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)$
77 40 76 mpd ${⊢}{\phi }\to \exists {e}\in \left({{S}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}$
78 1 3ad2ant1 ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to {S}\in \mathrm{SAlg}$
79 27 3ad2ant1 ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to {D}\in \mathrm{V}$
80 1 adantr ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\right)\to {S}\in \mathrm{SAlg}$
81 nnct ${⊢}ℕ\preccurlyeq \mathrm{\omega }$
82 81 a1i ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\right)\to ℕ\preccurlyeq \mathrm{\omega }$
83 elmapi ${⊢}{e}\in \left({{S}}^{ℕ}\right)\to {e}:ℕ⟶{S}$
84 83 adantl ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\right)\to {e}:ℕ⟶{S}$
85 84 ffvelrnda ${⊢}\left(\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\right)\wedge {n}\in ℕ\right)\to {e}\left({n}\right)\in {S}$
86 80 82 85 saliuncl ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\right)\to \bigcup _{{n}\in ℕ}{e}\left({n}\right)\in {S}$
87 86 3adant3 ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to \bigcup _{{n}\in ℕ}{e}\left({n}\right)\in {S}$
88 eqid ${⊢}\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}=\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}$
89 78 79 87 88 elrestd ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to \bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}\in \left({S}{↾}_{𝑡}{D}\right)$
90 nfra1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}$
91 rspa ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\wedge {n}\in ℕ\right)\to {F}\left({n}\right)={e}\left({n}\right)\cap {D}$
92 90 91 iuneq2df ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup _{{n}\in ℕ}\left({e}\left({n}\right)\cap {D}\right)$
93 iunin1 ${⊢}\bigcup _{{n}\in ℕ}\left({e}\left({n}\right)\cap {D}\right)=\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}$
94 93 a1i ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\to \bigcup _{{n}\in ℕ}\left({e}\left({n}\right)\cap {D}\right)=\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}$
95 92 94 eqtrd ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}$
96 95 3ad2ant3 ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}$
97 3 a1i ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to {T}={S}{↾}_{𝑡}{D}$
98 96 97 eleq12d ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to \left(\bigcup _{{n}\in ℕ}{F}\left({n}\right)\in {T}↔\bigcup _{{n}\in ℕ}{e}\left({n}\right)\cap {D}\in \left({S}{↾}_{𝑡}{D}\right)\right)$
99 89 98 mpbird ${⊢}\left({\phi }\wedge {e}\in \left({{S}}^{ℕ}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\right)\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)\in {T}$
100 99 3exp ${⊢}{\phi }\to \left({e}\in \left({{S}}^{ℕ}\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)\in {T}\right)\right)$
101 100 rexlimdv ${⊢}{\phi }\to \left(\exists {e}\in \left({{S}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={e}\left({n}\right)\cap {D}\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)\in {T}\right)$
102 77 101 mpd ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)\in {T}$