This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fneint

Description: If a cover is finer than another, every point can be approached more closely by intersections. (Contributed by Jeff Hankins, 11-Oct-2009)

Ref Expression
Assertion fneint 
|- ( A Fne B -> |^| { x e. B | P e. x } C_ |^| { x e. A | P e. x } )

Proof

Step Hyp Ref Expression
1 eleq2w 
 |-  ( x = y -> ( P e. x <-> P e. y ) )
2 1 elrab 
 |-  ( y e. { x e. A | P e. x } <-> ( y e. A /\ P e. y ) )
3 fnessex 
 |-  ( ( A Fne B /\ y e. A /\ P e. y ) -> E. z e. B ( P e. z /\ z C_ y ) )
4 3 3expb 
 |-  ( ( A Fne B /\ ( y e. A /\ P e. y ) ) -> E. z e. B ( P e. z /\ z C_ y ) )
5 eleq2w 
 |-  ( x = z -> ( P e. x <-> P e. z ) )
6 5 intminss 
 |-  ( ( z e. B /\ P e. z ) -> |^| { x e. B | P e. x } C_ z )
7 sstr 
 |-  ( ( |^| { x e. B | P e. x } C_ z /\ z C_ y ) -> |^| { x e. B | P e. x } C_ y )
8 6 7 sylan 
 |-  ( ( ( z e. B /\ P e. z ) /\ z C_ y ) -> |^| { x e. B | P e. x } C_ y )
9 8 expl 
 |-  ( z e. B -> ( ( P e. z /\ z C_ y ) -> |^| { x e. B | P e. x } C_ y ) )
10 9 rexlimiv 
 |-  ( E. z e. B ( P e. z /\ z C_ y ) -> |^| { x e. B | P e. x } C_ y )
11 4 10 syl 
 |-  ( ( A Fne B /\ ( y e. A /\ P e. y ) ) -> |^| { x e. B | P e. x } C_ y )
12 11 ex 
 |-  ( A Fne B -> ( ( y e. A /\ P e. y ) -> |^| { x e. B | P e. x } C_ y ) )
13 2 12 biimtrid 
 |-  ( A Fne B -> ( y e. { x e. A | P e. x } -> |^| { x e. B | P e. x } C_ y ) )
14 13 ralrimiv 
 |-  ( A Fne B -> A. y e. { x e. A | P e. x } |^| { x e. B | P e. x } C_ y )
15 ssint 
 |-  ( |^| { x e. B | P e. x } C_ |^| { x e. A | P e. x } <-> A. y e. { x e. A | P e. x } |^| { x e. B | P e. x } C_ y )
16 14 15 sylibr 
 |-  ( A Fne B -> |^| { x e. B | P e. x } C_ |^| { x e. A | P e. x } )