Metamath Proof Explorer

Theorem fnejoin1

Description: Join of equivalence classes under the fineness relation-part one. (Contributed by Jeff Hankins, 8-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion fnejoin1 
|- ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A Fne if ( S = (/) , { X } , U. S ) )

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( A e. S -> A C_ U. S )
2 1 3ad2ant3 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A C_ U. S )
3 2 unissd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. A C_ U. U. S )
4 eqimss2 
 |-  ( X = U. y -> U. y C_ X )
5 sspwuni 
 |-  ( y C_ ~P X <-> U. y C_ X )
6 4 5 sylibr 
 |-  ( X = U. y -> y C_ ~P X )
7 6 ralimi 
 |-  ( A. y e. S X = U. y -> A. y e. S y C_ ~P X )
8 7 3ad2ant2 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A. y e. S y C_ ~P X )
9 unissb 
 |-  ( U. S C_ ~P X <-> A. y e. S y C_ ~P X )
10 8 9 sylibr 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. S C_ ~P X )
11 sspwuni 
 |-  ( U. S C_ ~P X <-> U. U. S C_ X )
12 10 11 sylib 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. U. S C_ X )
13 unieq 
 |-  ( y = A -> U. y = U. A )
14 13 eqeq2d 
 |-  ( y = A -> ( X = U. y <-> X = U. A ) )
15 14 rspccva 
 |-  ( ( A. y e. S X = U. y /\ A e. S ) -> X = U. A )
16 15 3adant1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> X = U. A )
17 12 16 sseqtrd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. U. S C_ U. A )
18 3 17 eqssd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. A = U. U. S )
19 pwexg 
 |-  ( X e. V -> ~P X e. _V )
20 19 3ad2ant1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> ~P X e. _V )
21 20 10 ssexd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. S e. _V )
22 bastg 
 |-  ( U. S e. _V -> U. S C_ ( topGen ` U. S ) )
23 21 22 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. S C_ ( topGen ` U. S ) )
24 2 23 sstrd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A C_ ( topGen ` U. S ) )
25 eqid 
 |-  U. A = U. A
26 eqid 
 |-  U. U. S = U. U. S
27 25 26 isfne4 
 |-  ( A Fne U. S <-> ( U. A = U. U. S /\ A C_ ( topGen ` U. S ) ) )
28 18 24 27 sylanbrc 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A Fne U. S )
29 ne0i 
 |-  ( A e. S -> S =/= (/) )
30 29 3ad2ant3 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> S =/= (/) )
31 ifnefalse 
 |-  ( S =/= (/) -> if ( S = (/) , { X } , U. S ) = U. S )
32 30 31 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> if ( S = (/) , { X } , U. S ) = U. S )
33 28 32 breqtrrd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A Fne if ( S = (/) , { X } , U. S ) )