Metamath Proof Explorer

Theorem metnrmlem3

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
metdscn.j 
|- J = ( MetOpen ` D )
metnrmlem.1 
|- ( ph -> D e. ( *Met ` X ) )
metnrmlem.2 
|- ( ph -> S e. ( Clsd ` J ) )
metnrmlem.3 
|- ( ph -> T e. ( Clsd ` J ) )
metnrmlem.4 
|- ( ph -> ( S i^i T ) = (/) )
metnrmlem.u 
|- U = U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) )
metnrmlem.g 
|- G = ( x e. X |-> inf ( ran ( y e. T |-> ( x D y ) ) , RR* , < ) )
metnrmlem.v 
|- V = U_ s e. S ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) )
Assertion metnrmlem3 
|- ( ph -> E. z e. J E. w e. J ( S C_ z /\ T C_ w /\ ( z i^i w ) = (/) ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 metdscn.j 
 |-  J = ( MetOpen ` D )
3 metnrmlem.1 
 |-  ( ph -> D e. ( *Met ` X ) )
4 metnrmlem.2 
 |-  ( ph -> S e. ( Clsd ` J ) )
5 metnrmlem.3 
 |-  ( ph -> T e. ( Clsd ` J ) )
6 metnrmlem.4 
 |-  ( ph -> ( S i^i T ) = (/) )
7 metnrmlem.u 
 |-  U = U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) )
8 metnrmlem.g 
 |-  G = ( x e. X |-> inf ( ran ( y e. T |-> ( x D y ) ) , RR* , < ) )
9 metnrmlem.v 
 |-  V = U_ s e. S ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) )
10 incom 
 |-  ( T i^i S ) = ( S i^i T )
11 10 6 eqtrid 
 |-  ( ph -> ( T i^i S ) = (/) )
12 8 2 3 5 4 11 9 metnrmlem2 
 |-  ( ph -> ( V e. J /\ S C_ V ) )
13 12 simpld 
 |-  ( ph -> V e. J )
14 1 2 3 4 5 6 7 metnrmlem2 
 |-  ( ph -> ( U e. J /\ T C_ U ) )
15 14 simpld 
 |-  ( ph -> U e. J )
16 12 simprd 
 |-  ( ph -> S C_ V )
17 14 simprd 
 |-  ( ph -> T C_ U )
18 9 ineq1i 
 |-  ( V i^i U ) = ( U_ s e. S ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U )
19 iunin1 
 |-  U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) = ( U_ s e. S ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U )
20 18 19 eqtr4i 
 |-  ( V i^i U ) = U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U )
21 7 ineq2i 
 |-  ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) = ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
22 iunin2 
 |-  U_ t e. T ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) = ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
23 21 22 eqtr4i 
 |-  ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) = U_ t e. T ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
24 3 adantr 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> D e. ( *Met ` X ) )
25 eqid 
 |-  U. J = U. J
26 25 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ U. J )
27 4 26 syl 
 |-  ( ph -> S C_ U. J )
28 2 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
29 3 28 syl 
 |-  ( ph -> X = U. J )
30 27 29 sseqtrrd 
 |-  ( ph -> S C_ X )
31 30 sselda 
 |-  ( ( ph /\ s e. S ) -> s e. X )
32 31 adantrr 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> s e. X )
33 25 cldss 
 |-  ( T e. ( Clsd ` J ) -> T C_ U. J )
34 5 33 syl 
 |-  ( ph -> T C_ U. J )
35 34 29 sseqtrrd 
 |-  ( ph -> T C_ X )
36 35 sselda 
 |-  ( ( ph /\ t e. T ) -> t e. X )
37 36 adantrl 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> t e. X )
38 8 2 3 5 4 11 metnrmlem1a 
 |-  ( ( ph /\ s e. S ) -> ( 0 < ( G ` s ) /\ if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. RR+ ) )
39 38 simprd 
 |-  ( ( ph /\ s e. S ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. RR+ )
40 39 adantrr 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. RR+ )
41 40 rphalfcld 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) e. RR+ )
42 41 rpxrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) e. RR* )
43 1 2 3 4 5 6 metnrmlem1a 
 |-  ( ( ph /\ t e. T ) -> ( 0 < ( F ` t ) /\ if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR+ ) )
44 43 adantrl 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( 0 < ( F ` t ) /\ if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR+ ) )
45 44 simprd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR+ )
46 45 rphalfcld 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR+ )
47 46 rpxrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR* )
48 40 rpred 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. RR )
49 48 rehalfcld 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) e. RR )
50 45 rpred 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR )
51 50 rehalfcld 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR )
52 49 51 rexaddd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) +e ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) = ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) + ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
53 48 recnd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. CC )
54 50 recnd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. CC )
55 2cnd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> 2 e. CC )
56 2ne0 
 |-  2 =/= 0
57 56 a1i 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> 2 =/= 0 )
58 53 54 55 57 divdird 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) = ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) + ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
59 52 58 eqtr4d 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) +e ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) = ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) )
60 8 2 3 5 4 11 metnrmlem1 
 |-  ( ( ph /\ ( t e. T /\ s e. S ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) <_ ( t D s ) )
61 60 ancom2s 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) <_ ( t D s ) )
62 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ t e. X /\ s e. X ) -> ( t D s ) = ( s D t ) )
63 24 37 32 62 syl3anc 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( t D s ) = ( s D t ) )
64 61 63 breqtrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) <_ ( s D t ) )
65 1 2 3 4 5 6 metnrmlem1 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) <_ ( s D t ) )
66 40 rpxrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. RR* )
67 45 rpxrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR* )
68 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ s e. X /\ t e. X ) -> ( s D t ) e. RR* )
69 24 32 37 68 syl3anc 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( s D t ) e. RR* )
70 xle2add 
 |-  ( ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) e. RR* /\ if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR* ) /\ ( ( s D t ) e. RR* /\ ( s D t ) e. RR* ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) <_ ( s D t ) /\ if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) <_ ( s D t ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) +e if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) <_ ( ( s D t ) +e ( s D t ) ) ) )
71 66 67 69 69 70 syl22anc 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) <_ ( s D t ) /\ if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) <_ ( s D t ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) +e if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) <_ ( ( s D t ) +e ( s D t ) ) ) )
72 64 65 71 mp2and 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) +e if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) <_ ( ( s D t ) +e ( s D t ) ) )
73 48 50 readdcld 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) e. RR )
74 73 recnd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) e. CC )
75 74 55 57 divcan2d 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( 2 x. ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) = ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) )
76 2re 
 |-  2 e. RR
77 73 rehalfcld 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) e. RR )
78 rexmul 
 |-  ( ( 2 e. RR /\ ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) e. RR ) -> ( 2 *e ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) = ( 2 x. ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) )
79 76 77 78 sylancr 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( 2 *e ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) = ( 2 x. ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) )
80 48 50 rexaddd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) +e if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) = ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) )
81 75 79 80 3eqtr4d 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( 2 *e ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) = ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) +e if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) )
82 x2times 
 |-  ( ( s D t ) e. RR* -> ( 2 *e ( s D t ) ) = ( ( s D t ) +e ( s D t ) ) )
83 69 82 syl 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( 2 *e ( s D t ) ) = ( ( s D t ) +e ( s D t ) ) )
84 72 81 83 3brtr4d 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( 2 *e ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) <_ ( 2 *e ( s D t ) ) )
85 77 rexrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) e. RR* )
86 2rp 
 |-  2 e. RR+
87 86 a1i 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> 2 e. RR+ )
88 xlemul2 
 |-  ( ( ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) e. RR* /\ ( s D t ) e. RR* /\ 2 e. RR+ ) -> ( ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) <_ ( s D t ) <-> ( 2 *e ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) <_ ( 2 *e ( s D t ) ) ) )
89 85 69 87 88 syl3anc 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) <_ ( s D t ) <-> ( 2 *e ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) ) <_ ( 2 *e ( s D t ) ) ) )
90 84 89 mpbird 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) + if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) ) / 2 ) <_ ( s D t ) )
91 59 90 eqbrtrd 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) +e ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) <_ ( s D t ) )
92 bldisj 
 |-  ( ( ( D e. ( *Met ` X ) /\ s e. X /\ t e. X ) /\ ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) e. RR* /\ ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR* /\ ( ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) +e ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) <_ ( s D t ) ) ) -> ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) = (/) )
93 24 32 37 42 47 91 92 syl33anc 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) = (/) )
94 eqimss 
 |-  ( ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) = (/) -> ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) )
95 93 94 syl 
 |-  ( ( ph /\ ( s e. S /\ t e. T ) ) -> ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) )
96 95 anassrs 
 |-  ( ( ( ph /\ s e. S ) /\ t e. T ) -> ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) )
97 96 ralrimiva 
 |-  ( ( ph /\ s e. S ) -> A. t e. T ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) )
98 iunss 
 |-  ( U_ t e. T ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) <-> A. t e. T ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) )
99 97 98 sylibr 
 |-  ( ( ph /\ s e. S ) -> U_ t e. T ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) ) C_ (/) )
100 23 99 eqsstrid 
 |-  ( ( ph /\ s e. S ) -> ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) C_ (/) )
101 100 ralrimiva 
 |-  ( ph -> A. s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) C_ (/) )
102 iunss 
 |-  ( U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) C_ (/) <-> A. s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) C_ (/) )
103 101 102 sylibr 
 |-  ( ph -> U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) C_ (/) )
104 ss0 
 |-  ( U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) C_ (/) -> U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) = (/) )
105 103 104 syl 
 |-  ( ph -> U_ s e. S ( ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) ) i^i U ) = (/) )
106 20 105 eqtrid 
 |-  ( ph -> ( V i^i U ) = (/) )
107 sseq2 
 |-  ( z = V -> ( S C_ z <-> S C_ V ) )
108 ineq1 
 |-  ( z = V -> ( z i^i w ) = ( V i^i w ) )
109 108 eqeq1d 
 |-  ( z = V -> ( ( z i^i w ) = (/) <-> ( V i^i w ) = (/) ) )
110 107 109 3anbi13d 
 |-  ( z = V -> ( ( S C_ z /\ T C_ w /\ ( z i^i w ) = (/) ) <-> ( S C_ V /\ T C_ w /\ ( V i^i w ) = (/) ) ) )
111 sseq2 
 |-  ( w = U -> ( T C_ w <-> T C_ U ) )
112 ineq2 
 |-  ( w = U -> ( V i^i w ) = ( V i^i U ) )
113 112 eqeq1d 
 |-  ( w = U -> ( ( V i^i w ) = (/) <-> ( V i^i U ) = (/) ) )
114 111 113 3anbi23d 
 |-  ( w = U -> ( ( S C_ V /\ T C_ w /\ ( V i^i w ) = (/) ) <-> ( S C_ V /\ T C_ U /\ ( V i^i U ) = (/) ) ) )
115 110 114 rspc2ev 
 |-  ( ( V e. J /\ U e. J /\ ( S C_ V /\ T C_ U /\ ( V i^i U ) = (/) ) ) -> E. z e. J E. w e. J ( S C_ z /\ T C_ w /\ ( z i^i w ) = (/) ) )
116 13 15 16 17 106 115 syl113anc 
 |-  ( ph -> E. z e. J E. w e. J ( S C_ z /\ T C_ w /\ ( z i^i w ) = (/) ) )