Theorem smfsupdmmbl

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

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

Proof

Step	Hyp	Ref	Expression
1		smfsupdmmbl.1	|- F/ n ph
2		smfsupdmmbl.2	|- F/ x ph
3		smfsupdmmbl.3	|- F/_ x F
4		smfsupdmmbl.4	|- ( ph -> M e. ZZ )
5		smfsupdmmbl.5	|- Z = ( ZZ>= ` M )
6		smfsupdmmbl.6	|- ( ph -> S e. SAlg )
7		smfsupdmmbl.7	|- ( ph -> F : Z --> ( SMblFn ` S ) )
8		smfsupdmmbl.8	|- ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. S )
9		smfsupdmmbl.9	|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
10		smfsupdmmbl.10	|- G = ( x e. D |-> sup ( 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 ) | ( ( F ` n ) ` x ) < m } ) ) = ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
13	1 2 11 3 4 5 6 7 8 9 12 10	smfsupdmmbllem	|- ( ph -> dom G e. S )