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 ⊢ φ → A ∈ V
restuni6.2 ⊢ φ → B ∈ W
Assertion restuni6 ⊢ φ → ⋃ A ↾ 𝑡 B = ⋃ A ∩ B

Proof

Step Hyp Ref Expression
1 restuni6.1 ⊢ φ → A ∈ V
2 restuni6.2 ⊢ φ → B ∈ W
3 eqid ⊢ ⋃ A = ⋃ A
4 3 restin ⊢ A ∈ V ∧ B ∈ W → A ↾ 𝑡 B = A ↾ 𝑡 B ∩ ⋃ A
5 1 2 4 syl2anc ⊢ φ → A ↾ 𝑡 B = A ↾ 𝑡 B ∩ ⋃ A
6 5 unieqd ⊢ φ → ⋃ A ↾ 𝑡 B = ⋃ A ↾ 𝑡 B ∩ ⋃ A
7 inss2 ⊢ B ∩ ⋃ A ⊆ ⋃ A
8 7 a1i ⊢ φ → B ∩ ⋃ A ⊆ ⋃ A
9 1 8 restuni4 ⊢ φ → ⋃ A ↾ 𝑡 B ∩ ⋃ A = B ∩ ⋃ A
10 incom ⊢ B ∩ ⋃ A = ⋃ A ∩ B
11 10 a1i ⊢ φ → B ∩ ⋃ A = ⋃ A ∩ B
12 6 9 11 3eqtrd ⊢ φ → ⋃ A ↾ 𝑡 B = ⋃ A ∩ B