Metamath Proof Explorer

Theorem fsupdm

Description: The domain of the sup function is defined in Proposition 121F (b) of Fremlin1, p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in Fremlin1, p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses fsupdm.1 
|- F/ n ph
fsupdm.2 
|- F/ x ph
fsupdm.3 
|- F/ m ph
fsupdm.4 
|- F/_ x F
fsupdm.5 
|- ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR* )
fsupdm.6 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
fsupdm.7 
|- H = ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
Assertion fsupdm 
|- ( ph -> D = U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) )

Proof

Step Hyp Ref Expression
1 fsupdm.1 
 |-  F/ n ph
2 fsupdm.2 
 |-  F/ x ph
3 fsupdm.3 
 |-  F/ m ph
4 fsupdm.4 
 |-  F/_ x F
5 fsupdm.5 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR* )
6 fsupdm.6 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
7 fsupdm.7 
 |-  H = ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
8 nfcv 
 |-  F/_ x NN
9 nfcv 
 |-  F/_ x Z
10 nfrab1 
 |-  F/_ x { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m }
11 8 10 nfmpt 
 |-  F/_ x ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } )
12 9 11 nfmpt 
 |-  F/_ x ( n e. Z |-> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
13 7 12 nfcxfr 
 |-  F/_ x H
14 nfcv 
 |-  F/_ x n
15 13 14 nffv 
 |-  F/_ x ( H ` n )
16 nfcv 
 |-  F/_ x m
17 15 16 nffv 
 |-  F/_ x ( ( H ` n ) ` m )
18 9 17 nfiin 
 |-  F/_ x |^|_ n e. Z ( ( H ` n ) ` m )
19 8 18 nfiun 
 |-  F/_ x U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m )
20 nfv 
 |-  F/ m x e. |^|_ n e. Z dom ( F ` n )
21 3 20 nfan 
 |-  F/ m ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) )
22 nfv 
 |-  F/ m y e. RR
23 21 22 nfan 
 |-  F/ m ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR )
24 nfv 
 |-  F/ m A. n e. Z ( ( F ` n ) ` x ) <_ y
25 23 24 nfan 
 |-  F/ m ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y )
26 nfii1 
 |-  F/_ n |^|_ n e. Z dom ( F ` n )
27 26 nfcri 
 |-  F/ n x e. |^|_ n e. Z dom ( F ` n )
28 1 27 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) )
29 nfv 
 |-  F/ n y e. RR
30 28 29 nfan 
 |-  F/ n ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR )
31 nfra1 
 |-  F/ n A. n e. Z ( ( F ` n ) ` x ) <_ y
32 30 31 nfan 
 |-  F/ n ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y )
33 nfv 
 |-  F/ n m e. NN
34 nfv 
 |-  F/ n y < m
35 32 33 34 nf3an 
 |-  F/ n ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m )
36 vex 
 |-  x e. _V
37 36 a1i 
 |-  ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) -> x e. _V )
38 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ n e. Z ) -> x e. |^|_ n e. Z dom ( F ` n ) )
39 38 3ad2antl1 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> x e. |^|_ n e. Z dom ( F ` n ) )
40 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> n e. Z )
41 eliinid 
 |-  ( ( x e. |^|_ n e. Z dom ( F ` n ) /\ n e. Z ) -> x e. dom ( F ` n ) )
42 39 40 41 syl2anc 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> x e. dom ( F ` n ) )
43 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ n e. Z ) -> ph )
44 43 3ad2antl1 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> ph )
45 44 40 5 syl2anc 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR* )
46 45 42 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR* )
47 simpllr 
 |-  ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ n e. Z ) -> y e. RR )
48 47 rexrd 
 |-  ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ n e. Z ) -> y e. RR* )
49 48 3ad2antl1 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> y e. RR* )
50 simpl2 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> m e. NN )
51 50 nnxrd 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> m e. RR* )
52 simpl1r 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> A. n e. Z ( ( F ` n ) ` x ) <_ y )
53 rspa 
 |-  ( ( A. n e. Z ( ( F ` n ) ` x ) <_ y /\ n e. Z ) -> ( ( F ` n ) ` x ) <_ y )
54 52 40 53 syl2anc 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> ( ( F ` n ) ` x ) <_ y )
55 simpl3 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> y < m )
56 46 49 51 54 55 xrlelttrd 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> ( ( F ` n ) ` x ) < m )
57 42 56 rabidd 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> x e. { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } )
58 trud 
 |-  ( n e. Z -> T. )
59 id 
 |-  ( n e. Z -> n e. Z )
60 nfcv 
 |-  F/_ n Z
61 nnex 
 |-  NN e. _V
62 61 mptex 
 |-  ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) e. _V
63 62 a1i 
 |-  ( ( T. /\ n e. Z ) -> ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) e. _V )
64 60 7 63 fvmpt2df 
 |-  ( ( T. /\ n e. Z ) -> ( H ` n ) = ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
65 58 59 64 syl2anc 
 |-  ( n e. Z -> ( H ` n ) = ( m e. NN |-> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } ) )
66 4 14 nffv 
 |-  F/_ x ( F ` n )
67 66 nfdm 
 |-  F/_ x dom ( F ` n )
68 fvex 
 |-  ( F ` n ) e. _V
69 68 dmex 
 |-  dom ( F ` n ) e. _V
70 67 69 rabexf 
 |-  { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } e. _V
71 70 a1i 
 |-  ( ( n e. Z /\ m e. NN ) -> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } e. _V )
72 65 71 fvmpt2d 
 |-  ( ( n e. Z /\ m e. NN ) -> ( ( H ` n ) ` m ) = { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } )
73 72 eqcomd 
 |-  ( ( n e. Z /\ m e. NN ) -> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } = ( ( H ` n ) ` m ) )
74 40 50 73 syl2anc 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } = ( ( H ` n ) ` m ) )
75 57 74 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) /\ n e. Z ) -> x e. ( ( H ` n ) ` m ) )
76 35 37 75 eliind2 
 |-  ( ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) /\ m e. NN /\ y < m ) -> x e. |^|_ n e. Z ( ( H ` n ) ` m ) )
77 arch 
 |-  ( y e. RR -> E. m e. NN y < m )
78 77 ad2antlr 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) -> E. m e. NN y < m )
79 25 76 78 reximdd 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR ) /\ A. n e. Z ( ( F ` n ) ` x ) <_ y ) -> E. m e. NN x e. |^|_ n e. Z ( ( H ` n ) ` m ) )
80 79 rexlimdva2 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y -> E. m e. NN x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) )
81 80 3impia 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) /\ E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y ) -> E. m e. NN x e. |^|_ n e. Z ( ( H ` n ) ` m ) )
82 eliun 
 |-  ( x e. U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) <-> E. m e. NN x e. |^|_ n e. Z ( ( H ` n ) ` m ) )
83 81 82 sylibr 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) /\ E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y ) -> x e. U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) )
84 2 19 83 rabssd 
 |-  ( ph -> { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } C_ U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) )
85 6 84 eqsstrid 
 |-  ( ph -> D C_ U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) )
86 nfcv 
 |-  F/_ m D
87 nfv 
 |-  F/ x m e. NN
88 2 87 nfan 
 |-  F/ x ( ph /\ m e. NN )
89 nfrab1 
 |-  F/_ x { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
90 6 89 nfcxfr 
 |-  F/_ x D
91 1 33 nfan 
 |-  F/ n ( ph /\ m e. NN )
92 nfii1 
 |-  F/_ n |^|_ n e. Z ( ( H ` n ) ` m )
93 92 nfcri 
 |-  F/ n x e. |^|_ n e. Z ( ( H ` n ) ` m )
94 91 93 nfan 
 |-  F/ n ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) )
95 36 a1i 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> x e. _V )
96 eliinid 
 |-  ( ( x e. |^|_ n e. Z ( ( H ` n ) ` m ) /\ n e. Z ) -> x e. ( ( H ` n ) ` m ) )
97 96 adantll 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> x e. ( ( H ` n ) ` m ) )
98 simpr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> n e. Z )
99 simpllr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> m e. NN )
100 98 99 72 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> ( ( H ` n ) ` m ) = { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } )
101 97 100 eleqtrd 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> x e. { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } )
102 rabidim1 
 |-  ( x e. { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } -> x e. dom ( F ` n ) )
103 101 102 syl 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> x e. dom ( F ` n ) )
104 94 95 103 eliind2 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> x e. |^|_ n e. Z dom ( F ` n ) )
105 nnre 
 |-  ( m e. NN -> m e. RR )
106 105 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> m e. RR )
107 breq2 
 |-  ( y = m -> ( ( ( F ` n ) ` x ) <_ y <-> ( ( F ` n ) ` x ) <_ m ) )
108 107 ralbidv 
 |-  ( y = m -> ( A. n e. Z ( ( F ` n ) ` x ) <_ y <-> A. n e. Z ( ( F ` n ) ` x ) <_ m ) )
109 108 adantl 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ y = m ) -> ( A. n e. Z ( ( F ` n ) ` x ) <_ y <-> A. n e. Z ( ( F ` n ) ` x ) <_ m ) )
110 simplll 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> ph )
111 5 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> ( F ` n ) : dom ( F ` n ) --> RR* )
112 simp3 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> x e. dom ( F ` n ) )
113 111 112 ffvelcdmd 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> ( ( F ` n ) ` x ) e. RR* )
114 110 98 103 113 syl3anc 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR* )
115 99 nnxrd 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> m e. RR* )
116 rabidim2 
 |-  ( x e. { x e. dom ( F ` n ) | ( ( F ` n ) ` x ) < m } -> ( ( F ` n ) ` x ) < m )
117 101 116 syl 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) < m )
118 114 115 117 xrltled 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) <_ m )
119 94 118 ralrimia 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> A. n e. Z ( ( F ` n ) ` x ) <_ m )
120 106 109 119 rspcedvd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
121 104 120 rabidd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } )
122 121 6 eleqtrrdi 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. |^|_ n e. Z ( ( H ` n ) ` m ) ) -> x e. D )
123 88 18 90 122 ssdf2 
 |-  ( ( ph /\ m e. NN ) -> |^|_ n e. Z ( ( H ` n ) ` m ) C_ D )
124 3 86 123 iunssdf 
 |-  ( ph -> U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) C_ D )
125 85 124 eqssd 
 |-  ( ph -> D = U_ m e. NN |^|_ n e. Z ( ( H ` n ) ` m ) )