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 | |
|
subsalsal.2 | |
||
subsalsal.3 | |
||
Assertion | subsalsal | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subsalsal.1 | |
|
2 | subsalsal.2 | |
|
3 | subsalsal.3 | |
|
4 | 3 | ovexi | |
5 | 4 | a1i | |
6 | 1 | 0sald | |
7 | 0in | |
|
8 | 7 | eqcomi | |
9 | 1 2 6 8 | elrestd | |
10 | 9 3 | eleqtrrdi | |
11 | eqid | |
|
12 | id | |
|
13 | 12 3 | eleqtrdi | |
14 | 13 | adantl | |
15 | elrest | |
|
16 | 1 2 15 | syl2anc | |
17 | 16 | adantr | |
18 | 14 17 | mpbid | |
19 | 1 | adantr | |
20 | 19 | 3adant3 | |
21 | 2 | 3ad2ant1 | |
22 | simpr | |
|
23 | 19 22 | saldifcld | |
24 | 23 | 3adant3 | |
25 | eqid | |
|
26 | 20 21 24 25 | elrestd | |
27 | 3 | unieqi | |
28 | 27 | a1i | |
29 | 1 2 | restuni3 | |
30 | 28 29 | eqtrd | |
31 | 30 | adantr | |
32 | simpr | |
|
33 | 31 32 | difeq12d | |
34 | indifdir | |
|
35 | 34 | eqcomi | |
36 | 35 | a1i | |
37 | 33 36 | eqtrd | |
38 | 3 | a1i | |
39 | 37 38 | eleq12d | |
40 | 39 | 3adant2 | |
41 | 26 40 | mpbird | |
42 | 41 | 3exp | |
43 | 42 | rexlimdv | |
44 | 43 | adantr | |
45 | 18 44 | mpd | |
46 | 1 | adantr | |
47 | 2 | adantr | |
48 | simpr | |
|
49 | 46 47 3 48 | subsaliuncl | |
50 | 5 10 11 45 49 | issalnnd | |