Theorem issmf

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (i) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	issmf.s	|- ( ph -> S e. SAlg )
	issmf.d	|- D = dom F
Assertion	issmf	|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issmf.s	|- ( ph -> S e. SAlg )
2		issmf.d	|- D = dom F
3	1 2	issmflem	|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) < b } e. ( S |`t D ) ) ) )
4		breq2	|- ( b = a -> ( ( F ` y ) < b <-> ( F ` y ) < a ) )
5	4	rabbidv	|- ( b = a -> { y e. D | ( F ` y ) < b } = { y e. D | ( F ` y ) < a } )
6	5	eleq1d	|- ( b = a -> ( { y e. D | ( F ` y ) < b } e. ( S |`t D ) <-> { y e. D | ( F ` y ) < a } e. ( S |`t D ) ) )
7		fveq2	|- ( y = x -> ( F ` y ) = ( F ` x ) )
8	7	breq1d	|- ( y = x -> ( ( F ` y ) < a <-> ( F ` x ) < a ) )
9	8	cbvrabv	|- { y e. D | ( F ` y ) < a } = { x e. D | ( F ` x ) < a }
10	9	eleq1i	|- ( { y e. D | ( F ` y ) < a } e. ( S |`t D ) <-> { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
11	10	a1i	|- ( b = a -> ( { y e. D | ( F ` y ) < a } e. ( S |`t D ) <-> { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
12	6 11	bitrd	|- ( b = a -> ( { y e. D | ( F ` y ) < b } e. ( S |`t D ) <-> { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
13	12	cbvralvw	|- ( A. b e. RR { y e. D | ( F ` y ) < b } e. ( S |`t D ) <-> A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
14	13	3anbi3i	|- ( ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) < b } e. ( S |`t D ) ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
15	14	a1i	|- ( ph -> ( ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) < b } e. ( S |`t D ) ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )
16	3 15	bitrd	|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )