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 eqidd 
 |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) = ( n e. Z |-> ( x e. A |-> B ) ) )
12 11 8 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = ( x e. A |-> B ) )
13 12 dmeqd 
 |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = dom ( x e. A |-> B ) )
14 nfcv 
 |-  F/_ x Z
15 14 nfcri 
 |-  F/ x n e. Z
16 2 15 nfan 
 |-  F/ x ( ph /\ n e. Z )
17 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
18 7 3expa 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. V )
19 16 17 18 dmmptdf 
 |-  ( ( ph /\ n e. Z ) -> dom ( x e. A |-> B ) = A )
20 13 19 eqtr2d 
 |-  ( ( ph /\ n e. Z ) -> A = dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
21 1 20 iineq2d 
 |-  ( ph -> |^|_ n e. Z A = |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
22 2 21 rabeqd 
 |-  ( 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 } )
23 nfv 
 |-  F/ y x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
24 3 23 nfan 
 |-  F/ y ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
25 nfii1 
 |-  F/_ n |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
26 25 nfcri 
 |-  F/ n x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
27 1 26 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
28 simpll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ph )
29 simpr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> n e. Z )
30 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 ) )
31 30 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 ) )
32 13 19 eqtrd 
 |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A )
33 32 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 )
34 31 33 eleqtrd 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. A )
35 12 fveq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) )
36 35 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) )
37 simp3 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> x e. A )
38 fvmpt4 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
39 37 7 38 syl2anc 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
40 36 39 eqtr2d 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
41 40 breq2d 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( y <_ B <-> y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
42 28 29 34 41 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 ) ) )
43 27 42 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 ) ) )
44 24 43 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 ) ) )
45 2 44 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 ) } )
46 22 45 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 ) } )
47 9 46 eqtrid 
 |-  ( 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 ) } )
48 nfcv 
 |-  F/_ n RR
49 nfra1 
 |-  F/ n A. n e. Z y <_ B
50 48 49 nfrexw 
 |-  F/ n E. y e. RR A. n e. Z y <_ B
51 nfii1 
 |-  F/_ n |^|_ n e. Z A
52 50 51 nfrabw 
 |-  F/_ n { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B }
53 9 52 nfcxfr 
 |-  F/_ n D
54 53 nfcri 
 |-  F/ n x e. D
55 1 54 nfan 
 |-  F/ n ( ph /\ x e. D )
56 simpll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ph )
57 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> n e. Z )
58 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 )
59 58 9 eleq2s 
 |-  ( x e. D -> x e. |^|_ n e. Z A )
60 eliinid 
 |-  ( ( x e. |^|_ n e. Z A /\ n e. Z ) -> x e. A )
61 59 60 sylan 
 |-  ( ( x e. D /\ n e. Z ) -> x e. A )
62 61 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. A )
63 56 57 62 40 syl3anc 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
64 55 63 mpteq2da 
 |-  ( ( ph /\ x e. D ) -> ( n e. Z |-> B ) = ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
65 64 rneqd 
 |-  ( ( ph /\ x e. D ) -> ran ( n e. Z |-> B ) = ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
66 65 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 , < ) )
67 2 47 66 mpteq12da 
 |-  ( 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 , < ) ) )
68 10 67 eqtrid 
 |-  ( 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 , < ) ) )
69 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( x e. A |-> B ) )
70 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
71 14 70 nfmpt 
 |-  F/_ x ( n e. Z |-> ( x e. A |-> B ) )
72 1 8 fmptd2f 
 |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
73 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 ) }
74 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 , < ) )
75 69 71 4 5 6 72 73 74 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 ) )
76 68 75 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )