Theorem smfinfdmmbl

Description: If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025)

	Ref	Expression
Hypotheses	smfinfdmmbl.1	|- F/ n ph
	smfinfdmmbl.2	|- F/ x ph
	smfinfdmmbl.3	|- F/_ x F
	smfinfdmmbl.4	|- ( ph -> M e. ZZ )
	smfinfdmmbl.5	|- Z = ( ZZ>= ` M )
	smfinfdmmbl.6	|- ( ph -> S e. SAlg )
	smfinfdmmbl.7	|- ( ph -> F : Z --> ( SMblFn ` S ) )
	smfinfdmmbl.8	|- ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. S )
	smfinfdmmbl.9	|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
	smfinfdmmbl.10	|- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
Assertion	smfinfdmmbl	|- ( ph -> dom G e. S )

Proof

Step	Hyp	Ref	Expression
1		smfinfdmmbl.1	|- F/ n ph
2		smfinfdmmbl.2	|- F/ x ph
3		smfinfdmmbl.3	|- F/_ x F
4		smfinfdmmbl.4	|- ( ph -> M e. ZZ )
5		smfinfdmmbl.5	|- Z = ( ZZ>= ` M )
6		smfinfdmmbl.6	|- ( ph -> S e. SAlg )
7		smfinfdmmbl.7	|- ( ph -> F : Z --> ( SMblFn ` S ) )
8		smfinfdmmbl.8	|- ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. S )
9		smfinfdmmbl.9	|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
10		smfinfdmmbl.10	|- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
11		nfv	|- F/ m ph
12		eqid	|- ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) ) = ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) )
13	1 2 11 3 4 5 6 7 8 9 10 12	smfinfdmmbllem	|- ( ph -> dom G e. S )