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	$⊢ φ \to A \in V$
	restuni4.2	$⊢ φ \to B \subseteq ⋃ A$
Assertion	restuni4	$⊢ φ \to ⋃ (A ↾_{𝑡} B) = B$

Proof

Step	Hyp	Ref	Expression
1		restuni4.1	$⊢ φ \to A \in V$
2		restuni4.2	$⊢ φ \to B \subseteq ⋃ A$
3		incom	$⊢ B \cap ⋃ A = ⋃ A \cap B$
4	3	a1i	$⊢ φ \to B \cap ⋃ A = ⋃ A \cap B$
5		dfss	$⊢ B \subseteq ⋃ A \leftrightarrow B = B \cap ⋃ A$
6	2 5	sylib	$⊢ φ \to B = B \cap ⋃ A$
7	1	uniexd	$⊢ φ \to ⋃ A \in V$
8	7 2	ssexd	$⊢ φ \to B \in V$
9	1 8	restuni3	$⊢ φ \to ⋃ (A ↾_{𝑡} B) = ⋃ A \cap B$
10	4 6 9	3eqtr4rd	$⊢ φ \to ⋃ (A ↾_{𝑡} B) = B$

Metamath Proof Explorer

Theorem restuni4

Proof