Metamath Proof Explorer

Theorem sstotbnd3

Description: Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 
|- N = ( M |` ( Y X. Y ) )
Assertion sstotbnd3 
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )

Proof

Step Hyp Ref Expression
1 sstotbnd.2 
 |-  N = ( M |` ( Y X. Y ) )
2 1 sstotbnd2 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )
3 elin 
 |-  ( v e. ( ~P X i^i Fin ) <-> ( v e. ~P X /\ v e. Fin ) )
4 rabfi 
 |-  ( v e. Fin -> { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin )
5 4 anim2i 
 |-  ( ( v e. ~P X /\ v e. Fin ) -> ( v e. ~P X /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) )
6 3 5 sylbi 
 |-  ( v e. ( ~P X i^i Fin ) -> ( v e. ~P X /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) )
7 6 anim2i 
 |-  ( ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ v e. ( ~P X i^i Fin ) ) -> ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ ( v e. ~P X /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )
8 7 ancoms 
 |-  ( ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) d ) ) -> ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ ( v e. ~P X /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )
9 an12 
 |-  ( ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ ( v e. ~P X /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) <-> ( v e. ~P X /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )
10 8 9 sylib 
 |-  ( ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) d ) ) -> ( v e. ~P X /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )
11 10 reximi2 
 |-  ( E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) )
12 11 ralimi 
 |-  ( A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) )
13 2 12 syl6bi 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) -> A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )
14 ssrab2 
 |-  { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } C_ v
15 elpwi 
 |-  ( v e. ~P X -> v C_ X )
16 15 ad2antlr 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ v e. ~P X ) /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) -> v C_ X )
17 14 16 sstrid 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ v e. ~P X ) /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) -> { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } C_ X )
18 simprr 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ v e. ~P X ) /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) -> { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin )
19 elfpw 
 |-  ( { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. ( ~P X i^i Fin ) <-> ( { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } C_ X /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) )
20 17 18 19 sylanbrc 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ v e. ~P X ) /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) -> { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. ( ~P X i^i Fin ) )
21 ssel2 
 |-  ( ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ z e. Y ) -> z e. U_ x e. v ( x ( ball ` M ) d ) )
22 eliun 
 |-  ( z e. U_ x e. v ( x ( ball ` M ) d ) <-> E. x e. v z e. ( x ( ball ` M ) d ) )
23 21 22 sylib 
 |-  ( ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ z e. Y ) -> E. x e. v z e. ( x ( ball ` M ) d ) )
24 inelcm 
 |-  ( ( z e. ( x ( ball ` M ) d ) /\ z e. Y ) -> ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) )
25 24 expcom 
 |-  ( z e. Y -> ( z e. ( x ( ball ` M ) d ) -> ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) ) )
26 25 ancrd 
 |-  ( z e. Y -> ( z e. ( x ( ball ` M ) d ) -> ( ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) /\ z e. ( x ( ball ` M ) d ) ) ) )
27 26 reximdv 
 |-  ( z e. Y -> ( E. x e. v z e. ( x ( ball ` M ) d ) -> E. x e. v ( ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) /\ z e. ( x ( ball ` M ) d ) ) ) )
28 27 impcom 
 |-  ( ( E. x e. v z e. ( x ( ball ` M ) d ) /\ z e. Y ) -> E. x e. v ( ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) /\ z e. ( x ( ball ` M ) d ) ) )
29 23 28 sylancom 
 |-  ( ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ z e. Y ) -> E. x e. v ( ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) /\ z e. ( x ( ball ` M ) d ) ) )
30 eliun 
 |-  ( z e. U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) <-> E. y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } z e. ( y ( ball ` M ) d ) )
31 oveq1 
 |-  ( y = x -> ( y ( ball ` M ) d ) = ( x ( ball ` M ) d ) )
32 31 eleq2d 
 |-  ( y = x -> ( z e. ( y ( ball ` M ) d ) <-> z e. ( x ( ball ` M ) d ) ) )
33 32 rexrab2 
 |-  ( E. y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } z e. ( y ( ball ` M ) d ) <-> E. x e. v ( ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) /\ z e. ( x ( ball ` M ) d ) ) )
34 30 33 bitri 
 |-  ( z e. U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) <-> E. x e. v ( ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) /\ z e. ( x ( ball ` M ) d ) ) )
35 29 34 sylibr 
 |-  ( ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ z e. Y ) -> z e. U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) )
36 35 ex 
 |-  ( Y C_ U_ x e. v ( x ( ball ` M ) d ) -> ( z e. Y -> z e. U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) ) )
37 36 ssrdv 
 |-  ( Y C_ U_ x e. v ( x ( ball ` M ) d ) -> Y C_ U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) )
38 37 ad2antrl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ v e. ~P X ) /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) -> Y C_ U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) )
39 iuneq1 
 |-  ( w = { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } -> U_ y e. w ( y ( ball ` M ) d ) = U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) )
40 39 sseq2d 
 |-  ( w = { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } -> ( Y C_ U_ y e. w ( y ( ball ` M ) d ) <-> Y C_ U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) ) )
41 40 rspcev 
 |-  ( ( { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. ( ~P X i^i Fin ) /\ Y C_ U_ y e. { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } ( y ( ball ` M ) d ) ) -> E. w e. ( ~P X i^i Fin ) Y C_ U_ y e. w ( y ( ball ` M ) d ) )
42 20 38 41 syl2anc 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ v e. ~P X ) /\ ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) -> E. w e. ( ~P X i^i Fin ) Y C_ U_ y e. w ( y ( ball ` M ) d ) )
43 42 rexlimdva2 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) -> E. w e. ( ~P X i^i Fin ) Y C_ U_ y e. w ( y ( ball ` M ) d ) ) )
44 43 ralimdv 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) -> A. d e. RR+ E. w e. ( ~P X i^i Fin ) Y C_ U_ y e. w ( y ( ball ` M ) d ) ) )
45 1 sstotbnd2 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. w e. ( ~P X i^i Fin ) Y C_ U_ y e. w ( y ( ball ` M ) d ) ) )
46 44 45 sylibrd 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) -> N e. ( TotBnd ` Y ) ) )
47 13 46 impbid 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )