Metamath Proof Explorer

Theorem salrestss

Description: A sigma-algebra restricted to one of its elements is a subset of the original sigma-algebra. (Contributed by Glauco Siliprandi, 21-Dec-2024)

		Ref	Expression
	Hypotheses	salrestss.1	$⊢ φ \to S \in SAlg$
		salrestss.2	$⊢ φ \to E \in S$
	Assertion	salrestss	$⊢ φ \to S ↾_{𝑡} E \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		salrestss.1	$⊢ φ \to S \in SAlg$
2		salrestss.2	$⊢ φ \to E \in S$
3		simpr	$⊢ (φ \land x \in (S ↾_{𝑡} E)) \to x \in (S ↾_{𝑡} E)$
4	1	adantr	$⊢ (φ \land x \in (S ↾_{𝑡} E)) \to S \in SAlg$
5	2	adantr	$⊢ (φ \land x \in (S ↾_{𝑡} E)) \to E \in S$
6		elrest	$⊢ (S \in SAlg \land E \in S) \to (x \in (S ↾_{𝑡} E) \leftrightarrow \exists y \in S x = y \cap E)$
7	4 5 6	syl2anc	$⊢ (φ \land x \in (S ↾_{𝑡} E)) \to (x \in (S ↾_{𝑡} E) \leftrightarrow \exists y \in S x = y \cap E)$
8	3 7	mpbid	$⊢ (φ \land x \in (S ↾_{𝑡} E)) \to \exists y \in S x = y \cap E$
9		simprr	$⊢ (φ \land (y \in S \land x = y \cap E)) \to x = y \cap E$
10	1	adantr	$⊢ (φ \land y \in S) \to S \in SAlg$
11		simpr	$⊢ (φ \land y \in S) \to y \in S$
12	2	adantr	$⊢ (φ \land y \in S) \to E \in S$
13	10 11 12	salincld	$⊢ (φ \land y \in S) \to y \cap E \in S$
14	13	adantrr	$⊢ (φ \land (y \in S \land x = y \cap E)) \to y \cap E \in S$
15	9 14	eqeltrd	$⊢ (φ \land (y \in S \land x = y \cap E)) \to x \in S$
16	15	adantlr	$⊢ ((φ \land x \in (S ↾_{𝑡} E)) \land (y \in S \land x = y \cap E)) \to x \in S$
17	8 16	rexlimddv	$⊢ (φ \land x \in (S ↾_{𝑡} E)) \to x \in S$
18	17	ssd	$⊢ φ \to S ↾_{𝑡} E \subseteq S$