# 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 ) ) )`