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

Metamath Proof Explorer

Theorem restuni5

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
	Hypothesis	restuni5.1	$⊢ X = ⋃ J$
	Assertion	restuni5	$⊢ (J \in V \land A \subseteq X) \to A = ⋃ (J ↾_{𝑡} A)$

Proof

Step	Hyp	Ref	Expression
1		restuni5.1	$⊢ X = ⋃ J$
2		simpl	$⊢ (J \in V \land A \subseteq X) \to J \in V$
3		id	$⊢ A \subseteq X \to A \subseteq X$
4	3 1	sseqtrdi	$⊢ A \subseteq X \to A \subseteq ⋃ J$
5	4	adantl	$⊢ (J \in V \land A \subseteq X) \to A \subseteq ⋃ J$
6	2 5	restuni4	$⊢ (J \in V \land A \subseteq X) \to ⋃ (J ↾_{𝑡} A) = A$
7	6	eqcomd	$⊢ (J \in V \land A \subseteq X) \to A = ⋃ (J ↾_{𝑡} A)$