Theorem restuni4

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
Hypotheses	restuni4.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	restuni4.2	⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝐴 )
Assertion	restuni4	⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		restuni4.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		restuni4.2	⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝐴 )
3		incom	⊢ ( 𝐵 ∩ ∪ 𝐴 ) = ( ∪ 𝐴 ∩ 𝐵 )
4	3	a1i	⊢ ( 𝜑 → ( 𝐵 ∩ ∪ 𝐴 ) = ( ∪ 𝐴 ∩ 𝐵 ) )
5		dfss	⊢ ( 𝐵 ⊆ ∪ 𝐴 ↔ 𝐵 = ( 𝐵 ∩ ∪ 𝐴 ) )
6	2 5	sylib	⊢ ( 𝜑 → 𝐵 = ( 𝐵 ∩ ∪ 𝐴 ) )
7	1	uniexd	⊢ ( 𝜑 → ∪ 𝐴 ∈ V )
8	7 2	ssexd	⊢ ( 𝜑 → 𝐵 ∈ V )
9	1 8	restuni3	⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )
10	4 6 9	3eqtr4rd	⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = 𝐵 )