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 biimpi 
 |-  ( 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 ) ) ) )
147 146 adantr 
 |-  ( ( 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 ) ) ) )
148 simpr 
 |-  ( ( f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) /\ i e. X ) -> i e. X )
149 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 ) ) ) )
150 147 148 149 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 ) ) ) )
151 150 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 ) ) ) )
152 simpr 
 |-  ( ( ( ph /\ f e. |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> i e. X )
153 71 adantlr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( A ` i ) e. RR* )
154 85 adantlr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( B ` i ) e. RR* )
155 simpll 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ph )
156 eldifi 
 |-  ( f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
157 156 ad2antlr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
158 simpr 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> i e. X )
159 ioossre 
 |-  ( -oo (,) ( B ` i ) ) C_ RR
160 simplr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
161 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 ) )
162 160 161 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 ) )
163 simpr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> i e. X )
164 15 fvixp 
 |-  ( ( f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) /\ i e. X ) -> ( f ` i ) e. ( -oo (,) ( B ` i ) ) )
165 162 163 164 syl2anc 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. ( -oo (,) ( B ` i ) ) )
166 159 165 sselid 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. RR )
167 155 157 158 166 syl21anc 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. RR )
168 167 rexrd 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. RR* )
169 simpl 
 |-  ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ph )
170 156 adantl 
 |-  ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> f e. ( i ( H ` X ) ( B ` i ) ) )
171 169 170 jca 
 |-  ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) -> ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) )
172 171 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 ) ) ) )
173 simplr 
 |-  ( ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> i e. X )
174 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 ) )
175 ixpfn 
 |-  ( f e. X_ k e. X if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) -> f Fn X )
176 162 175 syl 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> f Fn X )
177 176 adantr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> f Fn X )
178 fveq2 
 |-  ( k = i -> ( f ` k ) = ( f ` i ) )
179 178 adantl 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k = i ) -> ( f ` k ) = ( f ` i ) )
180 23 a1i 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> -oo e. RR* )
181 71 ad4ant13 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( A ` i ) e. RR* )
182 166 adantr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) e. RR )
183 182 mnfltd 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> -oo < ( f ` i ) )
184 simpr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) < ( A ` i ) )
185 180 181 182 183 184 eliood 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> ( f ` i ) e. ( -oo (,) ( A ` i ) ) )
186 185 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k = i ) -> ( f ` i ) e. ( -oo (,) ( A ` i ) ) )
187 179 186 eqeltrd 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) /\ k = i ) -> ( f ` k ) e. ( -oo (,) ( A ` i ) ) )
188 187 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 ) ) )
189 78 eqcomd 
 |-  ( k = i -> ( -oo (,) ( A ` i ) ) = if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
190 189 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 ) )
191 188 190 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 ) )
192 15 159 eqsstrdi 
 |-  ( k = i -> if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) C_ RR )
193 ssid 
 |-  RR C_ RR
194 20 193 eqsstrdi 
 |-  ( -. k = i -> if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) C_ RR )
195 192 194 pm2.61i 
 |-  if ( k = i , ( -oo (,) ( B ` i ) ) , RR ) C_ RR
196 162 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 ) )
197 simpr 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> k e. X )
198 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 ) )
199 196 197 198 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 ) )
200 195 199 sselid 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) -> ( f ` k ) e. RR )
201 200 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ k e. X ) /\ -. k = i ) -> ( f ` k ) e. RR )
202 iffalse 
 |-  ( -. k = i -> if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) = RR )
203 202 eqcomd 
 |-  ( -. k = i -> RR = if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) )
204 203 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 ) )
205 201 204 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 ) )
206 205 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 ) )
207 191 206 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 ) )
208 207 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 ) )
209 177 208 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 ) ) )
210 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 ) ) )
211 209 210 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 ) )
212 74 eqcomd 
 |-  ( ( ph /\ i e. X ) -> X_ k e. X if ( k = i , ( -oo (,) ( A ` i ) ) , RR ) = ( i ( H ` X ) ( A ` i ) ) )
213 212 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 ) ) )
214 211 213 eleqtrd 
 |-  ( ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) /\ ( f ` i ) < ( A ` i ) ) -> f e. ( i ( H ` X ) ( A ` i ) ) )
215 172 173 174 214 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 ) ) )
216 eldifn 
 |-  ( f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) -> -. f e. ( i ( H ` X ) ( A ` i ) ) )
217 216 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 ) ) )
218 215 217 pm2.65da 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> -. ( f ` i ) < ( A ` i ) )
219 155 158 70 syl2anc 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( A ` i ) e. RR )
220 219 167 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 ) ) )
221 218 220 mpbird 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( A ` i ) <_ ( f ` i ) )
222 23 a1i 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> -oo e. RR* )
223 85 adantlr 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( B ` i ) e. RR* )
224 iooltub 
 |-  ( ( -oo e. RR* /\ ( B ` i ) e. RR* /\ ( f ` i ) e. ( -oo (,) ( B ` i ) ) ) -> ( f ` i ) < ( B ` i ) )
225 222 223 165 224 syl3anc 
 |-  ( ( ( ph /\ f e. ( i ( H ` X ) ( B ` i ) ) ) /\ i e. X ) -> ( f ` i ) < ( B ` i ) )
226 155 157 158 225 syl21anc 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) < ( B ` i ) )
227 153 154 168 221 226 elicod 
 |-  ( ( ( ph /\ f e. ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) /\ i e. X ) -> ( f ` i ) e. ( ( A ` i ) [,) ( B ` i ) ) )
228 145 151 152 227 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 ) ) )
229 228 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 ) ) ) )
230 144 229 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 ) ) )
231 141 230 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 ) ) ) )
232 231 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 ) ) )
233 232 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 ) ) ) )
234 110 233 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 ) ) ) ) )
235 234 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 ) ) ) ) )
236 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 ) ) ) ) )
237 235 236 sylibr 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) )