Metamath Proof Explorer

Theorem hspdifhsp

Description: A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspdifhsp.x 
|- ( ph -> X e. Fin )
hspdifhsp.n 
|- ( ph -> X =/= (/) )
hspdifhsp.a 
|- ( ph -> A : X --> RR )
hspdifhsp.b 
|- ( ph -> B : X --> RR )
hspdifhsp.h 
|- H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) )
Assertion hspdifhsp 
|- ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 hspdifhsp.x 
 |-  ( ph -> X e. Fin )
2 hspdifhsp.n 
 |-  ( ph -> X =/= (/) )
3 hspdifhsp.a 
 |-  ( ph -> A : X --> RR )
4 hspdifhsp.b 
 |-  ( ph -> B : X --> RR )
5 hspdifhsp.h 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) )
6 nfv 
 |-  F/ i ph
7 nfcv 
 |-  F/_ i f
8 nfixp1 
 |-  F/_ i X_ i e. X ( ( A ` i ) [,) ( B ` i ) )
9 7 8 nfel 
 |-  F/ i f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) )
10 6 9 nfan 
 |-  F/ i ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) )
11 ixpfn 
 |-  ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) -> f Fn X )
12 11 ad2antlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> f Fn X )
13 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
14 13 oveq2d 
 |-  ( k = i -> ( -oo (,) ( B ` k ) ) = ( -oo (,) ( B ` i ) ) )
15 iftrue 
 |-  ( k = i -> if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) = ( -oo (,) ( B ` i ) ) )
16 14 15 eqtr4d 
 |-  ( k = i -> ( -oo (,) ( B ` k ) ) = if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
17 eqimss 
 |-  ( ( -oo (,) ( B ` k ) ) = if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) -> ( -oo (,) ( B ` k ) ) C_ if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
18 16 17 syl 
 |-  ( k = i -> ( -oo (,) ( B ` k ) ) C_ if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
19 ioossre 
 |-  ( -oo (,) ( B ` k ) ) C_ RR
20 iffalse 
 |-  ( -. k = i -> if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) = RR )
21 19 20 sseqtrrid 
 |-  ( -. k = i -> ( -oo (,) ( B ` k ) ) C_ if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
22 18 21 pm2.61i 
 |-  ( -oo (,) ( B ` k ) ) C_ if ( k = i , ( -oo (,) ( B ` i ) ) , RR )
23 mnfxr 
 |-  -oo e. RR*
24 23 a1i 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> -oo e. RR* )
25 4 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
26 25 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
27 26 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( B ` k ) e. RR* )
28 3 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
29 icossre 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR* ) -> ( ( A ` k ) [,) ( B ` k ) ) C_ RR )
30 28 26 29 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( A ` k ) [,) ( B ` k ) ) C_ RR )
31 30 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( ( A ` k ) [,) ( B ` k ) ) C_ RR )
32 simpl 
 |-  ( ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) /\ k e. X ) -> f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) )
33 simpr 
 |-  ( ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) /\ k e. X ) -> k e. X )
34 fveq2 
 |-  ( i = k -> ( A ` i ) = ( A ` k ) )
35 fveq2 
 |-  ( i = k -> ( B ` i ) = ( B ` k ) )
36 34 35 oveq12d 
 |-  ( i = k -> ( ( A ` i ) [,) ( B ` i ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
37 36 fvixp 
 |-  ( ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) /\ k e. X ) -> ( f ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
38 32 33 37 syl2anc 
 |-  ( ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) /\ k e. X ) -> ( f ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
39 38 adantll 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( f ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
40 31 39 sseldd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( f ` k ) e. RR )
41 40 mnfltd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> -oo < ( f ` k ) )
42 28 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
43 42 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( A ` k ) e. RR* )
44 icoltub 
 |-  ( ( ( A ` k ) e. RR* /\ ( B ` k ) e. RR* /\ ( f ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) -> ( f ` k ) < ( B ` k ) )
45 43 27 39 44 syl3anc 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( f ` k ) < ( B ` k ) )
46 24 27 40 41 45 eliood 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( f ` k ) e. ( -oo (,) ( B ` k ) ) )
47 22 46 sselid 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ k e. X ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
48 47 adantlr 
 |-  ( ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
49 48 ralrimiva 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> A. k e. X ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
50 12 49 jca 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) ) )
51 vex 
 |-  f e. _V
52 51 elixp 
 |-  ( f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) <-> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) ) )
53 50 52 sylibr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
54 equequ1 
 |-  ( i = k -> ( i = l <-> k = l ) )
55 54 ifbid 
 |-  ( i = k -> if ( i = l , ( -oo (,) y ) , RR ) = if ( k = l , ( -oo (,) y ) , RR ) )
56 55 cbvixpv 
 |-  X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) = X_ k e. x if ( k = l , ( -oo (,) y ) , RR )
57 56 a1i 
 |-  ( ( l e. x /\ y e. RR ) -> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) = X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) )
58 57 mpoeq3ia 
 |-  ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) = ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) )
59 58 mpteq2i 
 |-  ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) ) = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
60 5 59 eqtri 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
61 1 adantr 
 |-  ( ( ph /\ i e. X ) -> X e. Fin )
62 simpr 
 |-  ( ( ph /\ i e. X ) -> i e. X )
63 4 adantr 
 |-  ( ( ph /\ i e. X ) -> B : X --> RR )
64 63 62 ffvelcdmd 
 |-  ( ( ph /\ i e. X ) -> ( B ` i ) e. RR )
65 60 61 62 64 hspval 
 |-  ( ( ph /\ i e. X ) -> ( i ( H ` X ) ( B ` i ) ) = X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
66 65 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( i ( H ` X ) ( B ` i ) ) = X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
67 53 66 eleqtrrd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
68 23 a1i 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> -oo e. RR* )
69 3 adantr 
 |-  ( ( ph /\ i e. X ) -> A : X --> RR )
70 69 62 ffvelcdmd 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) e. RR )
71 70 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) e. RR* )
72 71 adantr 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> ( A ` i ) e. RR* )
73 simpr 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> f e. ( i ( H ` X ) ( A ` i ) ) )
74 60 61 62 70 hspval 
 |-  ( ( ph /\ i e. X ) -> ( i ( H ` X ) ( A ` i ) ) = X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
75 74 adantr 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> ( i ( H ` X ) ( A ` i ) ) = X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
76 73 75 eleqtrd 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> f e. X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
77 62 adantr 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> i e. X )
78 iftrue 
 |-  ( k = i -> if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) = ( -oo (,) ( A ` i ) ) )
79 78 fvixp 
 |-  ( ( f e. X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) /\ i e. X ) -> ( f ` i ) e. ( -oo (,) ( A ` i ) ) )
80 76 77 79 syl2anc 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> ( f ` i ) e. ( -oo (,) ( A ` i ) ) )
81 iooltub 
 |-  ( ( -oo e. RR* /\ ( A ` i ) e. RR* /\ ( f ` i ) e. ( -oo (,) ( A ` i ) ) ) -> ( f ` i ) < ( A ` i ) )
82 68 72 80 81 syl3anc 
 |-  ( ( ( ph /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> ( f ` i ) < ( A ` i ) )
83 82 adantllr 
 |-  ( ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> ( f ` i ) < ( A ` i ) )
84 71 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( A ` i ) e. RR* )
85 64 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( B ` i ) e. RR* )
86 85 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( B ` i ) e. RR* )
87 51 elixp 
 |-  ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) <-> ( f Fn X /\ A. i e. X ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) ) )
88 87 biimpi 
 |-  ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) -> ( f Fn X /\ A. i e. X ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) ) )
89 88 simprd 
 |-  ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) -> A. i e. X ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
90 rspa 
 |-  ( ( A. i e. X ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) /\ i e. X ) -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
91 89 90 sylan 
 |-  ( ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) /\ i e. X ) -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
92 91 adantll 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
93 icogelb 
 |-  ( ( ( A ` i ) e. RR* /\ ( B ` i ) e. RR* /\ ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) ) -> ( A ` i ) <_ ( f ` i ) )
94 84 86 92 93 syl3anc 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( A ` i ) <_ ( f ` i ) )
95 70 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( A ` i ) e. RR )
96 icossre 
 |-  ( ( ( A ` i ) e. RR /\ ( B ` i ) e. RR* ) -> ( ( A ` i ) [,) ( B ` i ) ) C_ RR )
97 70 85 96 syl2anc 
 |-  ( ( ph /\ i e. X ) -> ( ( A ` i ) [,) ( B ` i ) ) C_ RR )
98 97 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( ( A ` i ) [,) ( B ` i ) ) C_ RR )
99 98 92 sseldd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. RR )
100 95 99 lenltd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> ( ( A ` i ) <_ ( f ` i ) <-> -. ( f ` i ) < ( A ` i ) ) )
101 94 100 mpbid 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> -. ( f ` i ) < ( A ` i ) )
102 101 adantr 
 |-  ( ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) /\ f e. ( i ( H ` X ) ( A ` i ) ) ) -> -. ( f ` i ) < ( A ` i ) )
103 83 102 pm2.65da 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> -. f e. ( i ( H ` X ) ( A ` i ) ) )
104 67 103 eldifd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) /\ i e. X ) -> f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
105 104 ex 
 |-  ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) -> ( i e. X -> f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) )
106 10 105 ralrimi 
 |-  ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) -> A. i e. X f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
107 eliin 
 |-  ( f e. _V -> ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) <-> A. i e. X f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) )
108 51 107 ax-mp 
 |-  ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) <-> A. i e. X f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
109 106 108 sylibr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) -> f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
110 109 ex 
 |-  ( ph -> ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) -> f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) )
111 n0 
 |-  ( X =/= (/) <-> E. k k e. X )
112 111 biimpi 
 |-  ( X =/= (/) -> E. k k e. X )
113 2 112 syl 
 |-  ( ph -> E. k k e. X )
114 113 adantr 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> E. k k e. X )
115 simpl 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ k e. X ) -> f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
116 simpr 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ k e. X ) -> k e. X )
117 id 
 |-  ( i = k -> i = k )
118 117 35 oveq12d 
 |-  ( i = k -> ( i ( H ` X ) ( B ` i ) ) = ( k ( H ` X ) ( B ` k ) ) )
119 117 34 oveq12d 
 |-  ( i = k -> ( i ( H ` X ) ( A ` i ) ) = ( k ( H ` X ) ( A ` k ) ) )
120 118 119 difeq12d 
 |-  ( i = k -> ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) = ( ( k ( H ` X ) ( B ` k ) ) \ ( k ( H ` X ) ( A ` k ) ) ) )
121 120 eleq2d 
 |-  ( i = k -> ( f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) <-> f e. ( ( k ( H ` X ) ( B ` k ) ) \ ( k ( H ` X ) ( A ` k ) ) ) ) )
122 115 116 121 eliind 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ k e. X ) -> f e. ( ( k ( H ` X ) ( B ` k ) ) \ ( k ( H ` X ) ( A ` k ) ) ) )
123 122 eldifad 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ k e. X ) -> f e. ( k ( H ` X ) ( B ` k ) ) )
124 123 adantll 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> f e. ( k ( H ` X ) ( B ` k ) ) )
125 equequ1 
 |-  ( i = h -> ( i = l <-> h = l ) )
126 125 ifbid 
 |-  ( i = h -> if ( i = l , ( -oo (,) y ) , RR ) = if ( h = l , ( -oo (,) y ) , RR ) )
127 126 cbvixpv 
 |-  X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) = X_ h e. x if ( h = l , ( -oo (,) y ) , RR )
128 127 a1i 
 |-  ( ( l e. x /\ y e. RR ) -> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) = X_ h e. x if ( h = l , ( -oo (,) y ) , RR ) )
129 128 mpoeq3ia 
 |-  ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) = ( l e. x , y e. RR |-> X_ h e. x if ( h = l , ( -oo (,) y ) , RR ) )
130 129 mpteq2i 
 |-  ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) ) = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ h e. x if ( h = l , ( -oo (,) y ) , RR ) ) )
131 5 130 eqtri 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ h e. x if ( h = l , ( -oo (,) y ) , RR ) ) )
132 1 ad2antrr 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> X e. Fin )
133 simpr 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> k e. X )
134 25 adantlr 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> ( B ` k ) e. RR )
135 131 132 133 134 hspval 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> ( k ( H ` X ) ( B ` k ) ) = X_ h e. X if ( h = k , ( -oo (,) ( B ` k ) ) , RR ) )
136 124 135 eleqtrd 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> f e. X_ h e. X if ( h = k , ( -oo (,) ( B ` k ) ) , RR ) )
137 ixpfn 
 |-  ( f e. X_ h e. X if ( h = k , ( -oo (,) ( B ` k ) ) , RR ) -> f Fn X )
138 136 137 syl 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ k e. X ) -> f Fn X )
139 138 ex 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ( k e. X -> f Fn X ) )
140 139 exlimdv 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ( E. k k e. X -> f Fn X ) )
141 114 140 mpd 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> f Fn X )
142 nfii1 
 |-  F/_ i |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) )
143 7 142 nfel 
 |-  F/ i f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) )
144 6 143 nfan 
 |-  F/ i ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
145 simpll 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ph )
146 108 birani 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ i e. X ) -> A. i e. X f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
147 simpr 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ i e. X ) -> i e. X )
148 rspa 
 |-  ( ( A. i e. X f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ i e. X ) -> f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
149 146 147 148 syl2anc 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ i e. X ) -> f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
150 149 adantll 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )
151 simpr 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> i e. X )
152 71 adantlr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( A ` i ) e. RR* )
153 85 adantlr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( B ` i ) e. RR* )
154 simpll 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ph )
155 eldifi 
 |-  ( f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
156 155 ad2antlr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
157 simpr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> i e. X )
158 ioossre 
 |-  ( -oo (,) ( B ` i ) ) C_ RR
159 simplr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
160 65 adantlr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( i ( H ` X ) ( B ` i ) ) = X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
161 159 160 eleqtrd 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
162 simpr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> i e. X )
163 15 fvixp 
 |-  ( ( f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) /\ i e. X ) -> ( f ` i ) e. ( -oo (,) ( B ` i ) ) )
164 161 162 163 syl2anc 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. ( -oo (,) ( B ` i ) ) )
165 158 164 sselid 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. RR )
166 154 156 157 165 syl21anc 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. RR )
167 166 rexrd 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. RR* )
168 simpl 
 |-  ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ph )
169 155 adantl 
 |-  ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
170 168 169 jca 
 |-  ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) )
171 170 ad2antrr 
 |-  ( ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) )
172 simplr 
 |-  ( ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> i e. X )
173 simpr 
 |-  ( ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) < ( A ` i ) )
174 ixpfn 
 |-  ( f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) -> f Fn X )
175 161 174 syl 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> f Fn X )
176 175 adantr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> f Fn X )
177 fveq2 
 |-  ( k = i -> ( f ` k ) = ( f ` i ) )
178 177 adantl 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k = i ) -> ( f ` k ) = ( f ` i ) )
179 23 a1i 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> -oo e. RR* )
180 71 ad4ant13 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( A ` i ) e. RR* )
181 165 adantr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) e. RR )
182 181 mnfltd 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> -oo < ( f ` i ) )
183 simpr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) < ( A ` i ) )
184 179 180 181 182 183 eliood 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) e. ( -oo (,) ( A ` i ) ) )
185 184 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k = i ) -> ( f ` i ) e. ( -oo (,) ( A ` i ) ) )
186 178 185 eqeltrd 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k = i ) -> ( f ` k ) e. ( -oo (,) ( A ` i ) ) )
187 186 adantlr 
 |-  ( ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k e. X ) /\ k = i ) -> ( f ` k ) e. ( -oo (,) ( A ` i ) ) )
188 78 eqcomd 
 |-  ( k = i -> ( -oo (,) ( A ` i ) ) = if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
189 188 adantl 
 |-  ( ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k e. X ) /\ k = i ) -> ( -oo (,) ( A ` i ) ) = if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
190 187 189 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k e. X ) /\ k = i ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
191 15 158 eqsstrdi 
 |-  ( k = i -> if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) C_ RR )
192 ssid 
 |-  RR C_ RR
193 20 192 eqsstrdi 
 |-  ( -. k = i -> if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) C_ RR )
194 191 193 pm2.61i 
 |-  if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) C_ RR
195 161 adantr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
196 simpr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> k e. X )
197 fvixp2 
 |-  ( ( f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) /\ k e. X ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
198 195 196 197 syl2anc 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) )
199 194 198 sselid 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> ( f ` k ) e. RR )
200 199 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) /\ -. k = i ) -> ( f ` k ) e. RR )
201 iffalse 
 |-  ( -. k = i -> if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) = RR )
202 201 eqcomd 
 |-  ( -. k = i -> RR = if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
203 202 adantl 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) /\ -. k = i ) -> RR = if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
204 200 203 eleqtrd 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) /\ -. k = i ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
205 204 adantllr 
 |-  ( ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k e. X ) /\ -. k = i ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
206 190 205 pm2.61dan 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k e. X ) -> ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
207 206 ralrimiva 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> A. k e. X ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
208 176 207 jca 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) ) )
209 51 elixp 
 |-  ( f e. X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) <-> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) ) )
210 208 209 sylibr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> f e. X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
211 74 eqcomd 
 |-  ( ( ph /\ i e. X ) -> X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) = ( i ( H ` X ) ( A ` i ) ) )
212 211 ad4ant13 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) = ( i ( H ` X ) ( A ` i ) ) )
213 210 212 eleqtrd 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> f e. ( i ( H ` X ) ( A ` i ) ) )
214 171 172 173 213 syl21anc 
 |-  ( ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> f e. ( i ( H ` X ) ( A ` i ) ) )
215 eldifn 
 |-  ( f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) -> -. f e. ( i ( H ` X ) ( A ` i ) ) )
216 215 ad3antlr 
 |-  ( ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> -. f e. ( i ( H ` X ) ( A ` i ) ) )
217 214 216 pm2.65da 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> -. ( f ` i ) < ( A ` i ) )
218 154 157 70 syl2anc 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( A ` i ) e. RR )
219 218 166 lenltd 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( ( A ` i ) <_ ( f ` i ) <-> -. ( f ` i ) < ( A ` i ) ) )
220 217 219 mpbird 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( A ` i ) <_ ( f ` i ) )
221 23 a1i 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> -oo e. RR* )
222 85 adantlr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( B ` i ) e. RR* )
223 iooltub 
 |-  ( ( -oo e. RR* /\ ( B ` i ) e. RR* /\ ( f ` i ) e. ( -oo (,) ( B ` i ) ) ) -> ( f ` i ) < ( B ` i ) )
224 221 222 164 223 syl3anc 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) < ( B ` i ) )
225 154 156 157 224 syl21anc 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) < ( B ` i ) )
226 152 153 167 220 225 elicod 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
227 145 150 151 226 syl21anc 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
228 227 ex 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ( i e. X -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) ) )
229 144 228 ralrimi 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> A. i e. X ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
230 141 229 jca 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ( f Fn X /\ A. i e. X ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) ) )
231 230 87 sylibr 
 |-  ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) )
232 231 ex 
 |-  ( ph -> ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) -> f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) ) )
233 110 232 impbid 
 |-  ( ph -> ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) <-> f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) )
234 233 alrimiv 
 |-  ( ph -> A. f ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) <-> f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) )
235 dfcleq 
 |-  ( X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) <-> A. f ( f e. X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) <-> f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) )
236 234 235 sylibr 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )