Metamath Proof Explorer

Theorem finfdm

Description: The domain of the inf function is defined in Proposition 121F (c) of Fremlin1, p. 39. See smfinf . Note that this definition of the inf 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 fifth statement of Proposition 121H in Fremlin1, p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025)

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

Proof

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