Metamath Proof Explorer

Theorem smfinfdmmbllem

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

Proof

Step Hyp Ref Expression
1 smfinfdmmbllem.1 
 |-  F/ n ph
2 smfinfdmmbllem.2 
 |-  F/ x ph
3 smfinfdmmbllem.3 
 |-  F/ m ph
4 smfinfdmmbllem.4 
 |-  F/_ x F
5 smfinfdmmbllem.5 
 |-  ( ph -> M e. ZZ )
6 smfinfdmmbllem.6 
 |-  Z = ( ZZ>= ` M )
7 smfinfdmmbllem.7 
 |-  ( ph -> S e. SAlg )
8 smfinfdmmbllem.8 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
9 smfinfdmmbllem.9 
 |-  ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. S )
10 smfinfdmmbllem.10 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
11 smfinfdmmbllem.11 
 |-  G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
12 smfinfdmmbllem.12 
 |-  H = ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) )
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 11 12 finfdm2 
 |-  ( 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 nnre 
 |-  ( m e. NN -> m e. RR )
41 40 renegcld 
 |-  ( m e. NN -> -u m e. RR )
42 41 rexrd 
 |-  ( m e. NN -> -u m e. RR* )
43 42 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> -u m e. RR* )
44 38 32 39 15 43 smfpimgtxr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } e. ( S |`t dom ( F ` n ) ) )
45 44 an32s 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. NN ) -> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } e. ( S |`t dom ( F ` n ) ) )
46 36 45 fmptd2f 
 |-  ( ( ph /\ n e. Z ) -> ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) : NN --> ( S |`t dom ( F ` n ) ) )
47 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
48 nnex 
 |-  NN e. _V
49 48 mptex 
 |-  ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) e. _V
50 12 fvmpt2 
 |-  ( ( n e. Z /\ ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) e. _V ) -> ( H ` n ) = ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) )
51 47 49 50 sylancl 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) )
52 51 feq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( H ` n ) : NN --> ( S |`t dom ( F ` n ) ) <-> ( m e. NN |-> { x e. dom ( F ` n ) | -u m < ( ( F ` n ) ` x ) } ) : NN --> ( S |`t dom ( F ` n ) ) ) )
53 46 52 mpbird 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) : NN --> ( S |`t dom ( F ` n ) ) )
54 53 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( H ` n ) : NN --> ( S |`t dom ( F ` n ) ) )
55 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> m e. NN )
56 54 55 ffvelcdmd 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( ( H ` n ) ` m ) e. ( S |`t dom ( F ` n ) ) )
57 34 56 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. Z ) -> ( ( H ` n ) ` m ) e. S )
58 24 25 26 27 29 31 57 saliinclf 
 |-  ( ( ph /\ m e. NN ) -> |^|_ n e. Z ( ( H ` n ) ` m ) e. S )
59 3 19 20 7 22 58 saliunclf 
 |-  ( ph -> U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) e. S )
60 18 59 eqeltrd 
 |-  ( ph -> dom G e. S )