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	syl5bi	|- ( 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 } )