Theorem subsaluni

Description: A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	subsaluni.1	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	subsaluni.2	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
Assertion	subsaluni	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		subsaluni.1	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		subsaluni.2	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
3	1 2	restuni4	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐴 ) = 𝐴 )
4	3	eqcomd	⊢ ( 𝜑 → 𝐴 = ∪ ( 𝑆 ↾t 𝐴 ) )
5	1	uniexd	⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
6	5 2	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
7		eqid	⊢ ( 𝑆 ↾t 𝐴 ) = ( 𝑆 ↾t 𝐴 )
8	1 6 7	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐴 ) ∈ SAlg )
9	8	salunid	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐴 ) ∈ ( 𝑆 ↾t 𝐴 ) )
10	4 9	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ↾t 𝐴 ) )