This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) )