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

Metamath Proof Explorer

Theorem restuni6

Description: The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses restuni6.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
restuni6.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion restuni6 ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 restuni6.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 restuni6.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
4 3 restin ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ↾t 𝐵 ) = ( 𝐴 ↾t ( 𝐵 ∩ ∪ 𝐴 ) ) )
5 1 2 4 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↾t 𝐵 ) = ( 𝐴 ↾t ( 𝐵 ∩ ∪ 𝐴 ) ) )
6 5 unieqd ⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ∪ ( 𝐴 ↾t ( 𝐵 ∩ ∪ 𝐴 ) ) )
7 inss2 ⊢ ( 𝐵 ∩ ∪ 𝐴 ) ⊆ ∪ 𝐴
8 7 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ ∪ 𝐴 ) ⊆ ∪ 𝐴 )
9 1 8 restuni4 ⊢ ( 𝜑 → ∪ ( 𝐴 ↾t ( 𝐵 ∩ ∪ 𝐴 ) ) = ( 𝐵 ∩ ∪ 𝐴 ) )
10 incom ⊢ ( 𝐵 ∩ ∪ 𝐴 ) = ( ∪ 𝐴 ∩ 𝐵 )
11 10 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ ∪ 𝐴 ) = ( ∪ 𝐴 ∩ 𝐵 ) )
12 6 9 11 3eqtrd ⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )