# Metamath Proof Explorer

## Theorem subsalsal

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

Ref Expression
Hypotheses subsalsal.1 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
subsalsal.2 ${⊢}{\phi }\to {D}\in {V}$
subsalsal.3 ${⊢}{T}={S}{↾}_{𝑡}{D}$
Assertion subsalsal ${⊢}{\phi }\to {T}\in \mathrm{SAlg}$

### Proof

Step Hyp Ref Expression
1 subsalsal.1 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
2 subsalsal.2 ${⊢}{\phi }\to {D}\in {V}$
3 subsalsal.3 ${⊢}{T}={S}{↾}_{𝑡}{D}$
4 3 ovexi ${⊢}{T}\in \mathrm{V}$
5 4 a1i ${⊢}{\phi }\to {T}\in \mathrm{V}$
6 1 0sald ${⊢}{\phi }\to \varnothing \in {S}$
7 0in ${⊢}\varnothing \cap {D}=\varnothing$
8 7 eqcomi ${⊢}\varnothing =\varnothing \cap {D}$
9 1 2 6 8 elrestd ${⊢}{\phi }\to \varnothing \in \left({S}{↾}_{𝑡}{D}\right)$
10 9 3 eleqtrrdi ${⊢}{\phi }\to \varnothing \in {T}$
11 eqid ${⊢}\bigcup {T}=\bigcup {T}$
12 id ${⊢}{x}\in {T}\to {x}\in {T}$
13 12 3 eleqtrdi ${⊢}{x}\in {T}\to {x}\in \left({S}{↾}_{𝑡}{D}\right)$
14 13 adantl ${⊢}\left({\phi }\wedge {x}\in {T}\right)\to {x}\in \left({S}{↾}_{𝑡}{D}\right)$
15 elrest ${⊢}\left({S}\in \mathrm{SAlg}\wedge {D}\in {V}\right)\to \left({x}\in \left({S}{↾}_{𝑡}{D}\right)↔\exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {D}\right)$
16 1 2 15 syl2anc ${⊢}{\phi }\to \left({x}\in \left({S}{↾}_{𝑡}{D}\right)↔\exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {D}\right)$
17 16 adantr ${⊢}\left({\phi }\wedge {x}\in {T}\right)\to \left({x}\in \left({S}{↾}_{𝑡}{D}\right)↔\exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {D}\right)$
18 14 17 mpbid ${⊢}\left({\phi }\wedge {x}\in {T}\right)\to \exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {D}$
19 1 adantr ${⊢}\left({\phi }\wedge {y}\in {S}\right)\to {S}\in \mathrm{SAlg}$
20 19 3adant3 ${⊢}\left({\phi }\wedge {y}\in {S}\wedge {x}={y}\cap {D}\right)\to {S}\in \mathrm{SAlg}$
21 2 3ad2ant1 ${⊢}\left({\phi }\wedge {y}\in {S}\wedge {x}={y}\cap {D}\right)\to {D}\in {V}$
22 simpr ${⊢}\left({\phi }\wedge {y}\in {S}\right)\to {y}\in {S}$
23 19 22 saldifcld ${⊢}\left({\phi }\wedge {y}\in {S}\right)\to \bigcup {S}\setminus {y}\in {S}$
24 23 3adant3 ${⊢}\left({\phi }\wedge {y}\in {S}\wedge {x}={y}\cap {D}\right)\to \bigcup {S}\setminus {y}\in {S}$
25 eqid ${⊢}\left(\bigcup {S}\setminus {y}\right)\cap {D}=\left(\bigcup {S}\setminus {y}\right)\cap {D}$
26 20 21 24 25 elrestd ${⊢}\left({\phi }\wedge {y}\in {S}\wedge {x}={y}\cap {D}\right)\to \left(\bigcup {S}\setminus {y}\right)\cap {D}\in \left({S}{↾}_{𝑡}{D}\right)$
27 3 unieqi ${⊢}\bigcup {T}=\bigcup \left({S}{↾}_{𝑡}{D}\right)$
28 27 a1i ${⊢}{\phi }\to \bigcup {T}=\bigcup \left({S}{↾}_{𝑡}{D}\right)$
29 1 2 restuni3 ${⊢}{\phi }\to \bigcup \left({S}{↾}_{𝑡}{D}\right)=\bigcup {S}\cap {D}$
30 28 29 eqtrd ${⊢}{\phi }\to \bigcup {T}=\bigcup {S}\cap {D}$
31 30 adantr ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to \bigcup {T}=\bigcup {S}\cap {D}$
32 simpr ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to {x}={y}\cap {D}$
33 31 32 difeq12d ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to \bigcup {T}\setminus {x}=\left(\bigcup {S}\cap {D}\right)\setminus \left({y}\cap {D}\right)$
34 indifdir ${⊢}\left(\bigcup {S}\setminus {y}\right)\cap {D}=\left(\bigcup {S}\cap {D}\right)\setminus \left({y}\cap {D}\right)$
35 34 eqcomi ${⊢}\left(\bigcup {S}\cap {D}\right)\setminus \left({y}\cap {D}\right)=\left(\bigcup {S}\setminus {y}\right)\cap {D}$
36 35 a1i ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to \left(\bigcup {S}\cap {D}\right)\setminus \left({y}\cap {D}\right)=\left(\bigcup {S}\setminus {y}\right)\cap {D}$
37 33 36 eqtrd ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to \bigcup {T}\setminus {x}=\left(\bigcup {S}\setminus {y}\right)\cap {D}$
38 3 a1i ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to {T}={S}{↾}_{𝑡}{D}$
39 37 38 eleq12d ${⊢}\left({\phi }\wedge {x}={y}\cap {D}\right)\to \left(\bigcup {T}\setminus {x}\in {T}↔\left(\bigcup {S}\setminus {y}\right)\cap {D}\in \left({S}{↾}_{𝑡}{D}\right)\right)$
40 39 3adant2 ${⊢}\left({\phi }\wedge {y}\in {S}\wedge {x}={y}\cap {D}\right)\to \left(\bigcup {T}\setminus {x}\in {T}↔\left(\bigcup {S}\setminus {y}\right)\cap {D}\in \left({S}{↾}_{𝑡}{D}\right)\right)$
41 26 40 mpbird ${⊢}\left({\phi }\wedge {y}\in {S}\wedge {x}={y}\cap {D}\right)\to \bigcup {T}\setminus {x}\in {T}$
42 41 3exp ${⊢}{\phi }\to \left({y}\in {S}\to \left({x}={y}\cap {D}\to \bigcup {T}\setminus {x}\in {T}\right)\right)$
43 42 rexlimdv ${⊢}{\phi }\to \left(\exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {D}\to \bigcup {T}\setminus {x}\in {T}\right)$
44 43 adantr ${⊢}\left({\phi }\wedge {x}\in {T}\right)\to \left(\exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {D}\to \bigcup {T}\setminus {x}\in {T}\right)$
45 18 44 mpd ${⊢}\left({\phi }\wedge {x}\in {T}\right)\to \bigcup {T}\setminus {x}\in {T}$
46 1 adantr ${⊢}\left({\phi }\wedge {f}:ℕ⟶{T}\right)\to {S}\in \mathrm{SAlg}$
47 2 adantr ${⊢}\left({\phi }\wedge {f}:ℕ⟶{T}\right)\to {D}\in {V}$
48 simpr ${⊢}\left({\phi }\wedge {f}:ℕ⟶{T}\right)\to {f}:ℕ⟶{T}$
49 46 47 3 48 subsaliuncl ${⊢}\left({\phi }\wedge {f}:ℕ⟶{T}\right)\to \bigcup _{{n}\in ℕ}{f}\left({n}\right)\in {T}$
50 5 10 11 45 49 issalnnd ${⊢}{\phi }\to {T}\in \mathrm{SAlg}$