Metamath Proof Explorer

Theorem fnejoin2

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

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

Proof

Step Hyp Ref Expression
1 unisng 
 |-  ( X e. V -> U. { X } = X )
2 1 eqcomd 
 |-  ( X e. V -> X = U. { X } )
3 2 adantr 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> X = U. { X } )
4 iftrue 
 |-  ( S = (/) -> if ( S = (/) , { X } , U. S ) = { X } )
5 4 unieqd 
 |-  ( S = (/) -> U. if ( S = (/) , { X } , U. S ) = U. { X } )
6 5 eqeq2d 
 |-  ( S = (/) -> ( X = U. if ( S = (/) , { X } , U. S ) <-> X = U. { X } ) )
7 3 6 syl5ibrcom 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( S = (/) -> X = U. if ( S = (/) , { X } , U. S ) ) )
8 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
9 unieq 
 |-  ( y = x -> U. y = U. x )
10 9 eqeq2d 
 |-  ( y = x -> ( X = U. y <-> X = U. x ) )
11 10 rspccva 
 |-  ( ( A. y e. S X = U. y /\ x e. S ) -> X = U. x )
12 11 3adant1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> X = U. x )
13 fnejoin1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> x Fne if ( S = (/) , { X } , U. S ) )
14 eqid 
 |-  U. x = U. x
15 eqid 
 |-  U. if ( S = (/) , { X } , U. S ) = U. if ( S = (/) , { X } , U. S )
16 14 15 fnebas 
 |-  ( x Fne if ( S = (/) , { X } , U. S ) -> U. x = U. if ( S = (/) , { X } , U. S ) )
17 13 16 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> U. x = U. if ( S = (/) , { X } , U. S ) )
18 12 17 eqtrd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> X = U. if ( S = (/) , { X } , U. S ) )
19 18 3expia 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( x e. S -> X = U. if ( S = (/) , { X } , U. S ) ) )
20 19 exlimdv 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( E. x x e. S -> X = U. if ( S = (/) , { X } , U. S ) ) )
21 8 20 biimtrid 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( S =/= (/) -> X = U. if ( S = (/) , { X } , U. S ) ) )
22 7 21 pm2.61dne 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> X = U. if ( S = (/) , { X } , U. S ) )
23 eqid 
 |-  U. T = U. T
24 15 23 fnebas 
 |-  ( if ( S = (/) , { X } , U. S ) Fne T -> U. if ( S = (/) , { X } , U. S ) = U. T )
25 22 24 sylan9eq 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ if ( S = (/) , { X } , U. S ) Fne T ) -> X = U. T )
26 25 ex 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( if ( S = (/) , { X } , U. S ) Fne T -> X = U. T ) )
27 fnetr 
 |-  ( ( x Fne if ( S = (/) , { X } , U. S ) /\ if ( S = (/) , { X } , U. S ) Fne T ) -> x Fne T )
28 27 ex 
 |-  ( x Fne if ( S = (/) , { X } , U. S ) -> ( if ( S = (/) , { X } , U. S ) Fne T -> x Fne T ) )
29 13 28 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> ( if ( S = (/) , { X } , U. S ) Fne T -> x Fne T ) )
30 29 3expa 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ x e. S ) -> ( if ( S = (/) , { X } , U. S ) Fne T -> x Fne T ) )
31 30 ralrimdva 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( if ( S = (/) , { X } , U. S ) Fne T -> A. x e. S x Fne T ) )
32 26 31 jcad 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( if ( S = (/) , { X } , U. S ) Fne T -> ( X = U. T /\ A. x e. S x Fne T ) ) )
33 22 adantr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> X = U. if ( S = (/) , { X } , U. S ) )
34 simprl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> X = U. T )
35 33 34 eqtr3d 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> U. if ( S = (/) , { X } , U. S ) = U. T )
36 sseq1 
 |-  ( { X } = if ( S = (/) , { X } , U. S ) -> ( { X } C_ ( topGen ` T ) <-> if ( S = (/) , { X } , U. S ) C_ ( topGen ` T ) ) )
37 sseq1 
 |-  ( U. S = if ( S = (/) , { X } , U. S ) -> ( U. S C_ ( topGen ` T ) <-> if ( S = (/) , { X } , U. S ) C_ ( topGen ` T ) ) )
38 elex 
 |-  ( X e. V -> X e. _V )
39 38 ad2antrr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> X e. _V )
40 34 39 eqeltrrd 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> U. T e. _V )
41 uniexb 
 |-  ( T e. _V <-> U. T e. _V )
42 40 41 sylibr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> T e. _V )
43 ssid 
 |-  T C_ T
44 eltg3i 
 |-  ( ( T e. _V /\ T C_ T ) -> U. T e. ( topGen ` T ) )
45 42 43 44 sylancl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> U. T e. ( topGen ` T ) )
46 34 45 eqeltrd 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> X e. ( topGen ` T ) )
47 46 snssd 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> { X } C_ ( topGen ` T ) )
48 47 adantr 
 |-  ( ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) /\ S = (/) ) -> { X } C_ ( topGen ` T ) )
49 simplrr 
 |-  ( ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) /\ -. S = (/) ) -> A. x e. S x Fne T )
50 fnetg 
 |-  ( x Fne T -> x C_ ( topGen ` T ) )
51 50 ralimi 
 |-  ( A. x e. S x Fne T -> A. x e. S x C_ ( topGen ` T ) )
52 49 51 syl 
 |-  ( ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) /\ -. S = (/) ) -> A. x e. S x C_ ( topGen ` T ) )
53 unissb 
 |-  ( U. S C_ ( topGen ` T ) <-> A. x e. S x C_ ( topGen ` T ) )
54 52 53 sylibr 
 |-  ( ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) /\ -. S = (/) ) -> U. S C_ ( topGen ` T ) )
55 36 37 48 54 ifbothda 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> if ( S = (/) , { X } , U. S ) C_ ( topGen ` T ) )
56 15 23 isfne4 
 |-  ( if ( S = (/) , { X } , U. S ) Fne T <-> ( U. if ( S = (/) , { X } , U. S ) = U. T /\ if ( S = (/) , { X } , U. S ) C_ ( topGen ` T ) ) )
57 35 55 56 sylanbrc 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S x Fne T ) ) -> if ( S = (/) , { X } , U. S ) Fne T )
58 57 ex 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( ( X = U. T /\ A. x e. S x Fne T ) -> if ( S = (/) , { X } , U. S ) Fne T ) )
59 32 58 impbid 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( if ( S = (/) , { X } , U. S ) Fne T <-> ( X = U. T /\ A. x e. S x Fne T ) ) )