Metamath Proof Explorer

Theorem bcthlem1

Description: Lemma for bcth . Substitutions for the function F . (Contributed by Mario Carneiro, 9-Jan-2014)

Ref Expression
Hypotheses bcth.2 
|- J = ( MetOpen ` D )
bcthlem.4 
|- ( ph -> D e. ( CMet ` X ) )
bcthlem.5 
|- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )
Assertion bcthlem1 
|- ( ( ph /\ ( A e. NN /\ B e. ( X X. RR+ ) ) ) -> ( C e. ( A F B ) <-> ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 bcth.2 
 |-  J = ( MetOpen ` D )
2 bcthlem.4 
 |-  ( ph -> D e. ( CMet ` X ) )
3 bcthlem.5 
 |-  F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )
4 opabssxp 
 |-  { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } C_ ( X X. RR+ )
5 elfvdm 
 |-  ( D e. ( CMet ` X ) -> X e. dom CMet )
6 2 5 syl 
 |-  ( ph -> X e. dom CMet )
7 reex 
 |-  RR e. _V
8 rpssre 
 |-  RR+ C_ RR
9 7 8 ssexi 
 |-  RR+ e. _V
10 xpexg 
 |-  ( ( X e. dom CMet /\ RR+ e. _V ) -> ( X X. RR+ ) e. _V )
11 6 9 10 sylancl 
 |-  ( ph -> ( X X. RR+ ) e. _V )
12 ssexg 
 |-  ( ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } C_ ( X X. RR+ ) /\ ( X X. RR+ ) e. _V ) -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } e. _V )
13 4 11 12 sylancr 
 |-  ( ph -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } e. _V )
14 oveq2 
 |-  ( k = A -> ( 1 / k ) = ( 1 / A ) )
15 14 breq2d 
 |-  ( k = A -> ( r < ( 1 / k ) <-> r < ( 1 / A ) ) )
16 fveq2 
 |-  ( k = A -> ( M ` k ) = ( M ` A ) )
17 16 difeq2d 
 |-  ( k = A -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) = ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) )
18 17 sseq2d 
 |-  ( k = A -> ( ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) <-> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) )
19 15 18 anbi12d 
 |-  ( k = A -> ( ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) <-> ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) ) )
20 19 anbi2d 
 |-  ( k = A -> ( ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) <-> ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) ) ) )
21 20 opabbidv 
 |-  ( k = A -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } = { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) ) } )
22 fveq2 
 |-  ( z = B -> ( ( ball ` D ) ` z ) = ( ( ball ` D ) ` B ) )
23 22 difeq1d 
 |-  ( z = B -> ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) = ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) )
24 23 sseq2d 
 |-  ( z = B -> ( ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) <-> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) )
25 24 anbi2d 
 |-  ( z = B -> ( ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) <-> ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
26 25 anbi2d 
 |-  ( z = B -> ( ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) ) <-> ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) ) )
27 26 opabbidv 
 |-  ( z = B -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` A ) ) ) ) } = { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } )
28 21 27 3 ovmpog 
 |-  ( ( A e. NN /\ B e. ( X X. RR+ ) /\ { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } e. _V ) -> ( A F B ) = { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } )
29 13 28 syl3an3 
 |-  ( ( A e. NN /\ B e. ( X X. RR+ ) /\ ph ) -> ( A F B ) = { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } )
30 29 3expa 
 |-  ( ( ( A e. NN /\ B e. ( X X. RR+ ) ) /\ ph ) -> ( A F B ) = { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } )
31 30 ancoms 
 |-  ( ( ph /\ ( A e. NN /\ B e. ( X X. RR+ ) ) ) -> ( A F B ) = { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } )
32 31 eleq2d 
 |-  ( ( ph /\ ( A e. NN /\ B e. ( X X. RR+ ) ) ) -> ( C e. ( A F B ) <-> C e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } ) )
33 4 sseli 
 |-  ( C e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } -> C e. ( X X. RR+ ) )
34 simp1 
 |-  ( ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) -> C e. ( X X. RR+ ) )
35 1st2nd2 
 |-  ( C e. ( X X. RR+ ) -> C = <. ( 1st ` C ) , ( 2nd ` C ) >. )
36 35 eleq1d 
 |-  ( C e. ( X X. RR+ ) -> ( C e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } <-> <. ( 1st ` C ) , ( 2nd ` C ) >. e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } ) )
37 fvex 
 |-  ( 1st ` C ) e. _V
38 fvex 
 |-  ( 2nd ` C ) e. _V
39 eleq1 
 |-  ( x = ( 1st ` C ) -> ( x e. X <-> ( 1st ` C ) e. X ) )
40 eleq1 
 |-  ( r = ( 2nd ` C ) -> ( r e. RR+ <-> ( 2nd ` C ) e. RR+ ) )
41 39 40 bi2anan9 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( ( x e. X /\ r e. RR+ ) <-> ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) ) )
42 simpr 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> r = ( 2nd ` C ) )
43 42 breq1d 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( r < ( 1 / A ) <-> ( 2nd ` C ) < ( 1 / A ) ) )
44 oveq12 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( x ( ball ` D ) r ) = ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) )
45 44 fveq2d 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) = ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) )
46 45 sseq1d 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) <-> ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) )
47 43 46 anbi12d 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) <-> ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
48 41 47 anbi12d 
 |-  ( ( x = ( 1st ` C ) /\ r = ( 2nd ` C ) ) -> ( ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) <-> ( ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) ) )
49 37 38 48 opelopaba 
 |-  ( <. ( 1st ` C ) , ( 2nd ` C ) >. e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } <-> ( ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
50 36 49 bitrdi 
 |-  ( C e. ( X X. RR+ ) -> ( C e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } <-> ( ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) ) )
51 35 eleq1d 
 |-  ( C e. ( X X. RR+ ) -> ( C e. ( X X. RR+ ) <-> <. ( 1st ` C ) , ( 2nd ` C ) >. e. ( X X. RR+ ) ) )
52 opelxp 
 |-  ( <. ( 1st ` C ) , ( 2nd ` C ) >. e. ( X X. RR+ ) <-> ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) )
53 51 52 bitr2di 
 |-  ( C e. ( X X. RR+ ) -> ( ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) <-> C e. ( X X. RR+ ) ) )
54 df-ov 
 |-  ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) = ( ( ball ` D ) ` <. ( 1st ` C ) , ( 2nd ` C ) >. )
55 35 fveq2d 
 |-  ( C e. ( X X. RR+ ) -> ( ( ball ` D ) ` C ) = ( ( ball ` D ) ` <. ( 1st ` C ) , ( 2nd ` C ) >. ) )
56 54 55 eqtr4id 
 |-  ( C e. ( X X. RR+ ) -> ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) = ( ( ball ` D ) ` C ) )
57 56 fveq2d 
 |-  ( C e. ( X X. RR+ ) -> ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) = ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) )
58 57 sseq1d 
 |-  ( C e. ( X X. RR+ ) -> ( ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) <-> ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) )
59 58 anbi2d 
 |-  ( C e. ( X X. RR+ ) -> ( ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) <-> ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
60 53 59 anbi12d 
 |-  ( C e. ( X X. RR+ ) -> ( ( ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) <-> ( C e. ( X X. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) ) )
61 3anass 
 |-  ( ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) <-> ( C e. ( X X. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
62 60 61 bitr4di 
 |-  ( C e. ( X X. RR+ ) -> ( ( ( ( 1st ` C ) e. X /\ ( 2nd ` C ) e. RR+ ) /\ ( ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( 1st ` C ) ( ball ` D ) ( 2nd ` C ) ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) <-> ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
63 50 62 bitrd 
 |-  ( C e. ( X X. RR+ ) -> ( C e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } <-> ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
64 33 34 63 pm5.21nii 
 |-  ( C e. { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / A ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) } <-> ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) )
65 32 64 bitrdi 
 |-  ( ( ph /\ ( A e. NN /\ B e. ( X X. RR+ ) ) ) -> ( C e. ( A F B ) <-> ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )