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	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	subsalsal.2	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	subsalsal.3	⊢ 𝑇 = ( 𝑆 ↾t 𝐷 )
Assertion	subsalsal	⊢ ( 𝜑 → 𝑇 ∈ SAlg )

Proof

Step	Hyp	Ref	Expression
1		subsalsal.1	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		subsalsal.2	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		subsalsal.3	⊢ 𝑇 = ( 𝑆 ↾t 𝐷 )
4	3	ovexi	⊢ 𝑇 ∈ V
5	4	a1i	⊢ ( 𝜑 → 𝑇 ∈ V )
6	1	0sald	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
7		0in	⊢ ( ∅ ∩ 𝐷 ) = ∅
8	7	eqcomi	⊢ ∅ = ( ∅ ∩ 𝐷 )
9	1 2 6 8	elrestd	⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
10	9 3	eleqtrrdi	⊢ ( 𝜑 → ∅ ∈ 𝑇 )
11		eqid	⊢ ∪ 𝑇 = ∪ 𝑇
12		id	⊢ ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑇 )
13	12 3	eleqtrdi	⊢ ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑆 ↾t 𝐷 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑆 ↾t 𝐷 ) )
15		elrest	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐷 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑆 𝑥 = ( 𝑦 ∩ 𝐷 ) ) )
16	1 2 15	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑆 𝑥 = ( 𝑦 ∩ 𝐷 ) ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑆 𝑥 = ( 𝑦 ∩ 𝐷 ) ) )
18	14 17	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ∃ 𝑦 ∈ 𝑆 𝑥 = ( 𝑦 ∩ 𝐷 ) )
19	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ∈ SAlg )
20	19	3adant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → 𝑆 ∈ SAlg )
21	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → 𝐷 ∈ 𝑉 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
23	19 22	saldifcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 )
24	23	3adant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 )
25		eqid	⊢ ( ( ∪ 𝑆 ∖ 𝑦 ) ∩ 𝐷 ) = ( ( ∪ 𝑆 ∖ 𝑦 ) ∩ 𝐷 )
26	20 21 24 25	elrestd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → ( ( ∪ 𝑆 ∖ 𝑦 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) )
27	3	unieqi	⊢ ∪ 𝑇 = ∪ ( 𝑆 ↾t 𝐷 )
28	27	a1i	⊢ ( 𝜑 → ∪ 𝑇 = ∪ ( 𝑆 ↾t 𝐷 ) )
29	1 2	restuni3	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) = ( ∪ 𝑆 ∩ 𝐷 ) )
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	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → 𝑇 = ( 𝑆 ↾t 𝐷 ) )
39	37 38	eleq12d	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → ( ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 ↔ ( ( ∪ 𝑆 ∖ 𝑦 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
40	39	3adant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → ( ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 ↔ ( ( ∪ 𝑆 ∖ 𝑦 ) ∩ 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
41	26 40	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 = ( 𝑦 ∩ 𝐷 ) ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 )
42	41	3exp	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → ( 𝑥 = ( 𝑦 ∩ 𝐷 ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 ) ) )
43	42	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑆 𝑥 = ( 𝑦 ∩ 𝐷 ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ∃ 𝑦 ∈ 𝑆 𝑥 = ( 𝑦 ∩ 𝐷 ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 ) )
45	18 44	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 )
46	1	adantr	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ ⟶ 𝑇 ) → 𝑆 ∈ SAlg )
47	2	adantr	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ ⟶ 𝑇 ) → 𝐷 ∈ 𝑉 )
48		simpr	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ ⟶ 𝑇 ) → 𝑓 : ℕ ⟶ 𝑇 )
49	46 47 3 48	subsaliuncl	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ ⟶ 𝑇 ) → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ 𝑇 )
50	5 10 11 45 49	issalnnd	⊢ ( 𝜑 → 𝑇 ∈ SAlg )