Theorem fness

Description: A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009)

	Ref	Expression
Hypotheses	fness.1	|- X = U. A
	fness.2	|- Y = U. B
Assertion	fness	|- ( ( B e. C /\ A C_ B /\ X = Y ) -> A Fne B )

Proof

Step	Hyp	Ref	Expression
1		fness.1	|- X = U. A
2		fness.2	|- Y = U. B
3		simp3	|- ( ( B e. C /\ A C_ B /\ X = Y ) -> X = Y )
4		ssel2	|- ( ( A C_ B /\ x e. A ) -> x e. B )
5	4	3adant3	|- ( ( A C_ B /\ x e. A /\ y e. x ) -> x e. B )
6		simp3	|- ( ( A C_ B /\ x e. A /\ y e. x ) -> y e. x )
7		ssid	|- x C_ x
8	6 7	jctir	|- ( ( A C_ B /\ x e. A /\ y e. x ) -> ( y e. x /\ x C_ x ) )
9		elequ2	|- ( z = x -> ( y e. z <-> y e. x ) )
10		sseq1	|- ( z = x -> ( z C_ x <-> x C_ x ) )
11	9 10	anbi12d	|- ( z = x -> ( ( y e. z /\ z C_ x ) <-> ( y e. x /\ x C_ x ) ) )
12	11	rspcev	|- ( ( x e. B /\ ( y e. x /\ x C_ x ) ) -> E. z e. B ( y e. z /\ z C_ x ) )
13	5 8 12	syl2anc	|- ( ( A C_ B /\ x e. A /\ y e. x ) -> E. z e. B ( y e. z /\ z C_ x ) )
14	13	3expib	|- ( A C_ B -> ( ( x e. A /\ y e. x ) -> E. z e. B ( y e. z /\ z C_ x ) ) )
15	14	ralrimivv	|- ( A C_ B -> A. x e. A A. y e. x E. z e. B ( y e. z /\ z C_ x ) )
16	15	3ad2ant2	|- ( ( B e. C /\ A C_ B /\ X = Y ) -> A. x e. A A. y e. x E. z e. B ( y e. z /\ z C_ x ) )
17	1 2	isfne2	|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) ) )
18	17	3ad2ant1	|- ( ( B e. C /\ A C_ B /\ X = Y ) -> ( A Fne B <-> ( X = Y /\ A. x e. A A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) ) )
19	3 16 18	mpbir2and	|- ( ( B e. C /\ A C_ B /\ X = Y ) -> A Fne B )