Theorem restuni5

Description: The underlying set of a subspace induced by the ` |``t ` operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	restuni5.1	⊢ 𝑋 = ∪ 𝐽
Assertion	restuni5	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		restuni5.1	⊢ 𝑋 = ∪ 𝐽
2		simpl	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ) → 𝐽 ∈ 𝑉 )
3		id	⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋 )
4	3 1	sseqtrdi	⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ⊆ ∪ 𝐽 )
5	4	adantl	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ ∪ 𝐽 )
6	2 5	restuni4	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ) → ∪ ( 𝐽 ↾t 𝐴 ) = 𝐴 )
7	6	eqcomd	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )