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	|- ( ph -> S e. SAlg )
	salrestss.2	|- ( ph -> E e. S )
Assertion	salrestss	|- ( ph -> ( S |`t E ) C_ S )

Proof

Step	Hyp	Ref	Expression
1		salrestss.1	|- ( ph -> S e. SAlg )
2		salrestss.2	|- ( ph -> E e. S )
3		simpr	|- ( ( ph /\ x e. ( S |`t E ) ) -> x e. ( S |`t E ) )
4	1	adantr	|- ( ( ph /\ x e. ( S |`t E ) ) -> S e. SAlg )
5	2	adantr	|- ( ( ph /\ x e. ( S |`t E ) ) -> E e. S )
6		elrest	|- ( ( S e. SAlg /\ E e. S ) -> ( x e. ( S |`t E ) <-> E. y e. S x = ( y i^i E ) ) )
7	4 5 6	syl2anc	|- ( ( ph /\ x e. ( S |`t E ) ) -> ( x e. ( S |`t E ) <-> E. y e. S x = ( y i^i E ) ) )
8	3 7	mpbid	|- ( ( ph /\ x e. ( S |`t E ) ) -> E. y e. S x = ( y i^i E ) )
9		simprr	|- ( ( ph /\ ( y e. S /\ x = ( y i^i E ) ) ) -> x = ( y i^i E ) )
10	1	adantr	|- ( ( ph /\ y e. S ) -> S e. SAlg )
11		simpr	|- ( ( ph /\ y e. S ) -> y e. S )
12	2	adantr	|- ( ( ph /\ y e. S ) -> E e. S )
13	10 11 12	salincld	|- ( ( ph /\ y e. S ) -> ( y i^i E ) e. S )
14	13	adantrr	|- ( ( ph /\ ( y e. S /\ x = ( y i^i E ) ) ) -> ( y i^i E ) e. S )
15	9 14	eqeltrd	|- ( ( ph /\ ( y e. S /\ x = ( y i^i E ) ) ) -> x e. S )
16	15	adantlr	|- ( ( ( ph /\ x e. ( S |`t E ) ) /\ ( y e. S /\ x = ( y i^i E ) ) ) -> x e. S )
17	8 16	rexlimddv	|- ( ( ph /\ x e. ( S |`t E ) ) -> x e. S )
18	17	ssd	|- ( ph -> ( S |`t E ) C_ S )