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 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )