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

Metamath Proof Explorer

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 )