Theorem smflimlem5

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem5.1	|- ( ph -> M e. ZZ )
	smflimlem5.2	|- Z = ( ZZ>= ` M )
	smflimlem5.3	|- ( ph -> S e. SAlg )
	smflimlem5.4	|- ( ph -> F : Z --> ( SMblFn ` S ) )
	smflimlem5.5	|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
	smflimlem5.6	|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
	smflimlem5.7	|- ( ph -> A e. RR )
	smflimlem5.8	|- P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
	smflimlem5.9	|- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
	smflimlem5.10	|- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
	smflimlem5.11	|- ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
Assertion	smflimlem5	|- ( ph -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) )

Proof

Step	Hyp	Ref	Expression
1		smflimlem5.1	|- ( ph -> M e. ZZ )
2		smflimlem5.2	|- Z = ( ZZ>= ` M )
3		smflimlem5.3	|- ( ph -> S e. SAlg )
4		smflimlem5.4	|- ( ph -> F : Z --> ( SMblFn ` S ) )
5		smflimlem5.5	|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
6		smflimlem5.6	|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7		smflimlem5.7	|- ( ph -> A e. RR )
8		smflimlem5.8	|- P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
9		smflimlem5.9	|- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
10		smflimlem5.10	|- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
11		smflimlem5.11	|- ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
12	2 3 4 5 6 7 8 9 10 11	smflimlem2	|- ( ph -> { x e. D | ( G ` x ) <_ A } C_ ( D i^i I ) )
13	1 2 3 4 5 6 7 8 9 10 11	smflimlem4	|- ( ph -> ( D i^i I ) C_ { x e. D | ( G ` x ) <_ A } )
14	12 13	eqssd	|- ( ph -> { x e. D | ( G ` x ) <_ A } = ( D i^i I ) )
15	2 3 5 8 9 10 11	smflimlem1	|- ( ph -> ( D i^i I ) e. ( S |`t D ) )
16	14 15	eqeltrd	|- ( ph -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) )