Metamath Proof Explorer

Theorem smfsupdmmbllem

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

Proof

Step Hyp Ref Expression
1 smfsupdmmbllem.1 
 |-  F/ n ph
2 smfsupdmmbllem.2 
 |-  F/ x ph
3 smfsupdmmbllem.3 
 |-  F/ m ph
4 smfsupdmmbllem.4 
 |-  F/_ x F
5 smfsupdmmbllem.5 
 |-  ( ph -> M e. ZZ )
6 smfsupdmmbllem.6 
 |-  Z = ( ZZ>= ` M )
7 smfsupdmmbllem.7 
 |-  ( ph -> S e. SAlg )
8 smfsupdmmbllem.8 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
9 smfsupdmmbllem.9 
 |-  ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. S )
10 smfsupdmmbllem.10 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
11 smfsupdmmbllem.11 
 |-  H = ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
12 smfsupdmmbllem.12 
 |-  G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
13 7 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
14 8 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
15 eqid 
 |-  dom ( F ` n ) = dom ( F ` n )
16 13 14 15 smff 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
17 16 frexr 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR* )
18 1 2 3 4 17 10 12 11 fsupdm2 
 |-  ( ph -> dom G = U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) )
19 nfcv 
 |-  F/_ m S
20 nfcv 
 |-  F/_ m NN
21 nnct 
 |-  NN ~<_ _om
22 21 a1i 
 |-  ( ph -> NN ~<_ _om )
23 nfv 
 |-  F/ n m e. NN
24 1 23 nfan 
 |-  F/ n ( ph /\ m e. NN )
25 nfcv 
 |-  F/_ n S
26 nfcv 
 |-  F/_ n Z
27 7 adantr 
 |-  ( ( ph /\ m e. NN ) -> S e. SAlg )
28 6 uzct 
 |-  Z ~<_ _om
29 28 a1i 
 |-  ( ( ph /\ m e. NN ) -> Z ~<_ _om )
30 5 6 uzn0d 
 |-  ( ph -> Z =/= (/) )
31 30 adantr 
 |-  ( ( ph /\ m e. NN ) -> Z =/= (/) )
32 27 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> S e. SAlg )
33 9 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> dom ( F ` n ) e. S )
34 32 33 salrestss 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( S |`t dom ( F ` n ) ) C_ S )
35 nfv 
 |-  F/ m n e. Z
36 3 35 nfan 
 |-  F/ m ( ph /\ n e. Z )
37 nfcv 
 |-  F/_ x n
38 4 37 nffv 
 |-  F/_ x ( F ` n )
39 14 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
40 nnxr 
 |-  ( m e. NN -> m e. RR* )
41 40 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> m e. RR* )
42 38 32 39 15 41 smfpimltxr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } e. ( S |`t dom ( F ` n ) ) )
43 42 an32s 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. NN ) -> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } e. ( S |`t dom ( F ` n ) ) )
44 36 43 fmptd2f 
 |-  ( ( ph /\ n e. Z ) -> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) : NN --> ( S |`t dom ( F ` n ) ) )
45 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
46 nnex 
 |-  NN e. _V
47 46 mptex 
 |-  ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) e. _V
48 11 fvmpt2 
 |-  ( ( n e. Z /\ ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) e. _V ) -> ( H ` n ) = ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
49 45 47 48 sylancl 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
50 49 feq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( H ` n ) : NN --> ( S |`t dom ( F ` n ) ) <-> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) : NN --> ( S |`t dom ( F ` n ) ) ) )
51 44 50 mpbird 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) : NN --> ( S |`t dom ( F ` n ) ) )
52 51 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( H ` n ) : NN --> ( S |`t dom ( F ` n ) ) )
53 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> m e. NN )
54 52 53 ffvelcdmd 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( ( H ` n ) ` m ) e. ( S |`t dom ( F ` n ) ) )
55 34 54 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( ( H ` n ) ` m ) e. S )
56 24 25 26 27 29 31 55 saliinclf 
 |-  ( ( ph /\ m e. NN ) -> |^|_ n e. Z ( ( H ` n ) ` m ) e. S )
57 3 19 20 7 22 56 saliunclf 
 |-  ( ph -> U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) e. S )
58 18 57 eqeltrd 
 |-  ( ph -> dom G e. S )