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{\upharpoonright }_{𝑡}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{\upharpoonright }_{𝑡}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{\upharpoonright }_{𝑡}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{\upharpoonright }_{𝑡}D\right)$$
14	13	adantl	$$⊢\left(\phi \wedge x\in T\right)\to x\in \left(S{\upharpoonright }_{𝑡}D\right)$$
15		elrest	$$⊢\left(S\in \mathrm{SAlg}\wedge D\in V\right)\to \left(x\in \left(S{\upharpoonright }_{𝑡}D\right)\leftrightarrow \exists y\in Sx=y\cap D\right)$$
16	1 2 15	syl2anc	$$⊢\phi \to \left(x\in \left(S{\upharpoonright }_{𝑡}D\right)\leftrightarrow \exists y\in Sx=y\cap D\right)$$
17	16	adantr	$$⊢\left(\phi \wedge x\in T\right)\to \left(x\in \left(S{\upharpoonright }_{𝑡}D\right)\leftrightarrow \exists y\in Sx=y\cap D\right)$$
18	14 17	mpbid	$$⊢\left(\phi \wedge x\in T\right)\to \exists y\in Sx=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{\upharpoonright }_{𝑡}D\right)$$
27	3	unieqi	$$⊢\bigcup T=\bigcup \left(S{\upharpoonright }_{𝑡}D\right)$$
28	27	a1i	$$⊢\phi \to \bigcup T=\bigcup \left(S{\upharpoonright }_{𝑡}D\right)$$
29	1 2	restuni3	$$⊢\phi \to \bigcup \left(S{\upharpoonright }_{𝑡}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{\upharpoonright }_{𝑡}D$$
39	37 38	eleq12d	$$⊢\left(\phi \wedge x=y\cap D\right)\to \left(\bigcup T\setminus x\in T\leftrightarrow \left(\bigcup S\setminus y\right)\cap D\in \left(S{\upharpoonright }_{𝑡}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\leftrightarrow \left(\bigcup S\setminus y\right)\cap D\in \left(S{\upharpoonright }_{𝑡}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 Sx=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 Sx=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:\mathbb{N}⟶T\right)\to S\in \mathrm{SAlg}$$
47	2	adantr	$$⊢\left(\phi \wedge f:\mathbb{N}⟶T\right)\to D\in V$$
48		simpr	$$⊢\left(\phi \wedge f:\mathbb{N}⟶T\right)\to f:\mathbb{N}⟶T$$
49	46 47 3 48	subsaliuncl	$$⊢\left(\phi \wedge f:\mathbb{N}⟶T\right)\to \bigcup _{n\in \mathbb{N}}f\left(n\right)\in T$$
50	5 10 11 45 49	issalnnd	$$⊢\phi \to T\in \mathrm{SAlg}$$