Theorem smfpimioompt

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimioompt.x	|- F/ x ph
	smfpimioompt.s	|- ( ph -> S e. SAlg )
	smfpimioompt.a	|- ( ph -> A e. V )
	smfpimioompt.b	|- ( ( ph /\ x e. A ) -> B e. W )
	smfpimioompt.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
	smfpimioompt.l	|- ( ph -> L e. RR* )
	smfpimioompt.r	|- ( ph -> R e. RR* )
Assertion	smfpimioompt	|- ( ph -> { x e. A | B e. ( L (,) R ) } e. ( S |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimioompt.x	|- F/ x ph
2		smfpimioompt.s	|- ( ph -> S e. SAlg )
3		smfpimioompt.a	|- ( ph -> A e. V )
4		smfpimioompt.b	|- ( ( ph /\ x e. A ) -> B e. W )
5		smfpimioompt.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
6		smfpimioompt.l	|- ( ph -> L e. RR* )
7		smfpimioompt.r	|- ( ph -> R e. RR* )
8		eqid	|- dom ( x e. A |-> B ) = dom ( x e. A |-> B )
9	2 5 8	smff	|- ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR )
10		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
11	1 10 4	dmmptdf	|- ( ph -> dom ( x e. A |-> B ) = A )
12	11	feq2d	|- ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR <-> ( x e. A |-> B ) : A --> RR ) )
13	9 12	mpbid	|- ( ph -> ( x e. A |-> B ) : A --> RR )
14	13	fvmptelrn	|- ( ( ph /\ x e. A ) -> B e. RR )
15	14	rexrd	|- ( ( ph /\ x e. A ) -> B e. RR* )
16	1 6 7 15	pimiooltgt	|- ( ph -> { x e. A | B e. ( L (,) R ) } = ( { x e. A | B < R } i^i { x e. A | L < B } ) )
17		eqid	|- ( S |`t A ) = ( S |`t A )
18	2 3 17	subsalsal	|- ( ph -> ( S |`t A ) e. SAlg )
19	1 2 4 5 7	smfpimltxrmpt	|- ( ph -> { x e. A | B < R } e. ( S |`t A ) )
20	1 2 4 5 6	smfpimgtxrmpt	|- ( ph -> { x e. A | L < B } e. ( S |`t A ) )
21	18 19 20	salincld	|- ( ph -> ( { x e. A | B < R } i^i { x e. A | L < B } ) e. ( S |`t A ) )
22	16 21	eqeltrd	|- ( ph -> { x e. A | B e. ( L (,) R ) } e. ( S |`t A ) )