Metamath Proof Explorer

Theorem smfinfmpt

Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfinfmpt.n 
|- F/ n ph
smfinfmpt.x 
|- F/ x ph
smfinfmpt.y 
|- F/ y ph
smfinfmpt.m 
|- ( ph -> M e. ZZ )
smfinfmpt.z 
|- Z = ( ZZ>= ` M )
smfinfmpt.s 
|- ( ph -> S e. SAlg )
smfinfmpt.b 
|- ( ( ph /\ n e. Z /\ x e. A ) -> B e. V )
smfinfmpt.f 
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfinfmpt.d 
|- D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B }
smfinfmpt.g 
|- G = ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) )
Assertion smfinfmpt 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfinfmpt.n 
 |-  F/ n ph
2 smfinfmpt.x 
 |-  F/ x ph
3 smfinfmpt.y 
 |-  F/ y ph
4 smfinfmpt.m 
 |-  ( ph -> M e. ZZ )
5 smfinfmpt.z 
 |-  Z = ( ZZ>= ` M )
6 smfinfmpt.s 
 |-  ( ph -> S e. SAlg )
7 smfinfmpt.b 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> B e. V )
8 smfinfmpt.f 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
9 smfinfmpt.d 
 |-  D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B }
10 smfinfmpt.g 
 |-  G = ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) )
11 10 a1i 
 |-  ( ph -> G = ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) )
12 9 a1i 
 |-  ( ph -> D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } )
13 eqidd 
 |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) = ( n e. Z |-> ( x e. A |-> B ) ) )
14 13 8 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = ( x e. A |-> B ) )
15 14 dmeqd 
 |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = dom ( x e. A |-> B ) )
16 nfcv 
 |-  F/_ x n
17 nfcv 
 |-  F/_ x Z
18 16 17 nfel 
 |-  F/ x n e. Z
19 2 18 nfan 
 |-  F/ x ( ph /\ n e. Z )
20 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
21 6 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
22 7 3expa 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. V )
23 19 21 22 8 smffmpt 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) : A --> RR )
24 23 fvmptelrn 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. RR )
25 19 20 24 dmmptdf 
 |-  ( ( ph /\ n e. Z ) -> dom ( x e. A |-> B ) = A )
26 eqidd 
 |-  ( ( ph /\ n e. Z ) -> A = A )
27 15 25 26 3eqtrrd 
 |-  ( ( ph /\ n e. Z ) -> A = dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
28 1 27 iineq2d 
 |-  ( ph -> |^|_ n e. Z A = |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
29 nfcv 
 |-  F/_ x |^|_ n e. Z A
30 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
31 17 30 nfmpt 
 |-  F/_ x ( n e. Z |-> ( x e. A |-> B ) )
32 31 16 nffv 
 |-  F/_ x ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
33 32 nfdm 
 |-  F/_ x dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
34 17 33 nfiin 
 |-  F/_ x |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
35 29 34 rabeqf 
 |-  ( |^|_ n e. Z A = |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ B } )
36 28 35 syl 
 |-  ( ph -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ B } )
37 nfv 
 |-  F/ y x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
38 3 37 nfan 
 |-  F/ y ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
39 nfcv 
 |-  F/_ n x
40 nfii1 
 |-  F/_ n |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
41 39 40 nfel 
 |-  F/ n x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
42 1 41 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
43 simpll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ph )
44 simpr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> n e. Z )
45 eliinid 
 |-  ( ( x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) /\ n e. Z ) -> x e. dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
46 45 adantll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
47 27 eqcomd 
 |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A )
48 47 adantlr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A )
49 46 48 eleqtrd 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. A )
50 14 fveq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) )
51 50 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) )
52 simp3 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> x e. A )
53 20 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
54 52 7 53 syl2anc 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
55 51 54 eqtr2d 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
56 55 breq2d 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( y <_ B <-> y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
57 43 44 49 56 syl3anc 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ( y <_ B <-> y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
58 42 57 ralbida 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) -> ( A. n e. Z y <_ B <-> A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
59 38 58 rexbid 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) -> ( E. y e. RR A. n e. Z y <_ B <-> E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
60 2 59 rabbida 
 |-  ( ph -> { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } )
61 36 60 eqtrd 
 |-  ( ph -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } )
62 12 61 eqtrd 
 |-  ( ph -> D = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } )
63 2 62 alrimi 
 |-  ( ph -> A. x D = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } )
64 nfcv 
 |-  F/_ n RR
65 nfra1 
 |-  F/ n A. n e. Z y <_ B
66 64 65 nfrex 
 |-  F/ n E. y e. RR A. n e. Z y <_ B
67 nfii1 
 |-  F/_ n |^|_ n e. Z A
68 66 67 nfrabw 
 |-  F/_ n { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B }
69 9 68 nfcxfr 
 |-  F/_ n D
70 39 69 nfel 
 |-  F/ n x e. D
71 1 70 nfan 
 |-  F/ n ( ph /\ x e. D )
72 simpll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ph )
73 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> n e. Z )
74 9 eleq2i 
 |-  ( x e. D <-> x e. { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } )
75 74 biimpi 
 |-  ( x e. D -> x e. { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } )
76 rabidim1 
 |-  ( x e. { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } -> x e. |^|_ n e. Z A )
77 75 76 syl 
 |-  ( x e. D -> x e. |^|_ n e. Z A )
78 77 adantr 
 |-  ( ( x e. D /\ n e. Z ) -> x e. |^|_ n e. Z A )
79 simpr 
 |-  ( ( x e. D /\ n e. Z ) -> n e. Z )
80 eliinid 
 |-  ( ( x e. |^|_ n e. Z A /\ n e. Z ) -> x e. A )
81 78 79 80 syl2anc 
 |-  ( ( x e. D /\ n e. Z ) -> x e. A )
82 81 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. A )
83 55 idi 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
84 72 73 82 83 syl3anc 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
85 71 84 mpteq2da 
 |-  ( ( ph /\ x e. D ) -> ( n e. Z |-> B ) = ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
86 85 rneqd 
 |-  ( ( ph /\ x e. D ) -> ran ( n e. Z |-> B ) = ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
87 86 infeq1d 
 |-  ( ( ph /\ x e. D ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) )
88 87 ex 
 |-  ( ph -> ( x e. D -> inf ( ran ( n e. Z |-> B ) , RR , < ) = inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) )
89 2 88 ralrimi 
 |-  ( ph -> A. x e. D inf ( ran ( n e. Z |-> B ) , RR , < ) = inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) )
90 mpteq12f 
 |-  ( ( A. x D = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } /\ A. x e. D inf ( ran ( n e. Z |-> B ) , RR , < ) = inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) -> ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) )
91 63 89 90 syl2anc 
 |-  ( ph -> ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) )
92 11 91 eqtrd 
 |-  ( ph -> G = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) )
93 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( x e. A |-> B ) )
94 eqid 
 |-  ( n e. Z |-> ( x e. A |-> B ) ) = ( n e. Z |-> ( x e. A |-> B ) )
95 1 8 94 fmptdf 
 |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
96 eqid 
 |-  { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) }
97 eqid 
 |-  ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) )
98 93 31 4 5 6 95 96 97 smfinf 
 |-  ( ph -> ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) )
99 92 98 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )