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 φSSAlg
subsalsal.2 φDV
subsalsal.3 T=S𝑡D
Assertion subsalsal φTSAlg

Proof

Step Hyp Ref Expression
1 subsalsal.1 φSSAlg
2 subsalsal.2 φDV
3 subsalsal.3 T=S𝑡D
4 3 ovexi TV
5 4 a1i φTV
6 1 0sald φS
7 0in D=
8 7 eqcomi =D
9 1 2 6 8 elrestd φS𝑡D
10 9 3 eleqtrrdi φT
11 eqid T=T
12 id xTxT
13 12 3 eleqtrdi xTxS𝑡D
14 13 adantl φxTxS𝑡D
15 elrest SSAlgDVxS𝑡DySx=yD
16 1 2 15 syl2anc φxS𝑡DySx=yD
17 16 adantr φxTxS𝑡DySx=yD
18 14 17 mpbid φxTySx=yD
19 1 adantr φySSSAlg
20 19 3adant3 φySx=yDSSAlg
21 2 3ad2ant1 φySx=yDDV
22 simpr φySyS
23 19 22 saldifcld φySSyS
24 23 3adant3 φySx=yDSyS
25 eqid SyD=SyD
26 20 21 24 25 elrestd φySx=yDSyDS𝑡D
27 3 unieqi T=S𝑡D
28 27 a1i φT=S𝑡D
29 1 2 restuni3 φS𝑡D=SD
30 28 29 eqtrd φT=SD
31 30 adantr φx=yDT=SD
32 simpr φx=yDx=yD
33 31 32 difeq12d φx=yDTx=SDyD
34 indifdir SyD=SDyD
35 34 eqcomi SDyD=SyD
36 35 a1i φx=yDSDyD=SyD
37 33 36 eqtrd φx=yDTx=SyD
38 3 a1i φx=yDT=S𝑡D
39 37 38 eleq12d φx=yDTxTSyDS𝑡D
40 39 3adant2 φySx=yDTxTSyDS𝑡D
41 26 40 mpbird φySx=yDTxT
42 41 3exp φySx=yDTxT
43 42 rexlimdv φySx=yDTxT
44 43 adantr φxTySx=yDTxT
45 18 44 mpd φxTTxT
46 1 adantr φf:TSSAlg
47 2 adantr φf:TDV
48 simpr φf:Tf:T
49 46 47 3 48 subsaliuncl φf:TnfnT
50 5 10 11 45 49 issalnnd φTSAlg