Metamath Proof Explorer

Theorem fnemeet2

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

Ref Expression
Assertion fnemeet2 
|- ( ( X e. V /\ A. y e. S X = U. y ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) <-> ( X = U. T /\ A. x e. S T Fne x ) ) )

Proof

Step Hyp Ref Expression
1 riin0 
 |-  ( S = (/) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = ~P X )
2 1 unieqd 
 |-  ( S = (/) -> U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = U. ~P X )
3 unipw 
 |-  U. ~P X = X
4 2 3 eqtr2di 
 |-  ( S = (/) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
5 4 a1i 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( S = (/) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
6 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
7 unieq 
 |-  ( y = x -> U. y = U. x )
8 7 eqeq2d 
 |-  ( y = x -> ( X = U. y <-> X = U. x ) )
9 8 rspccva 
 |-  ( ( A. y e. S X = U. y /\ x e. S ) -> X = U. x )
10 9 3adant1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> X = U. x )
11 fnemeet1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) Fne x )
12 eqid 
 |-  U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) )
13 eqid 
 |-  U. x = U. x
14 12 13 fnebas 
 |-  ( ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) Fne x -> U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = U. x )
15 11 14 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = U. x )
16 10 15 eqtr4d 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
17 16 3expia 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( x e. S -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
18 17 exlimdv 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( E. x x e. S -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
19 6 18 syl5bi 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( S =/= (/) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
20 5 19 pm2.61dne 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
21 20 adantr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
22 eqid 
 |-  U. T = U. T
23 22 12 fnebas 
 |-  ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> U. T = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
24 23 adantl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) -> U. T = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
25 21 24 eqtr4d 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) -> X = U. T )
26 25 ex 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> X = U. T ) )
27 fnetr 
 |-  ( ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) /\ ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) Fne x ) -> T Fne x )
28 27 expcom 
 |-  ( ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) Fne x -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> T Fne x ) )
29 11 28 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ x e. S ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> T Fne x ) )
30 29 3expa 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ x e. S ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> T Fne x ) )
31 30 ralrimdva 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> A. x e. S T Fne x ) )
32 26 31 jcad 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) -> ( X = U. T /\ A. x e. S T Fne x ) ) )
33 simprl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> X = U. T )
34 20 adantr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> X = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
35 33 34 eqtr3d 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> U. T = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
36 eqimss2 
 |-  ( X = U. T -> U. T C_ X )
37 36 ad2antrl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> U. T C_ X )
38 sspwuni 
 |-  ( T C_ ~P X <-> U. T C_ X )
39 37 38 sylibr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> T C_ ~P X )
40 breq2 
 |-  ( x = t -> ( T Fne x <-> T Fne t ) )
41 40 cbvralvw 
 |-  ( A. x e. S T Fne x <-> A. t e. S T Fne t )
42 fnetg 
 |-  ( T Fne t -> T C_ ( topGen ` t ) )
43 42 ralimi 
 |-  ( A. t e. S T Fne t -> A. t e. S T C_ ( topGen ` t ) )
44 41 43 sylbi 
 |-  ( A. x e. S T Fne x -> A. t e. S T C_ ( topGen ` t ) )
45 44 ad2antll 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> A. t e. S T C_ ( topGen ` t ) )
46 ssiin 
 |-  ( T C_ |^|_ t e. S ( topGen ` t ) <-> A. t e. S T C_ ( topGen ` t ) )
47 45 46 sylibr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> T C_ |^|_ t e. S ( topGen ` t ) )
48 39 47 ssind 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> T C_ ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
49 pwexg 
 |-  ( X e. V -> ~P X e. _V )
50 inex1g 
 |-  ( ~P X e. _V -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) e. _V )
51 49 50 syl 
 |-  ( X e. V -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) e. _V )
52 51 ad2antrr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) e. _V )
53 bastg 
 |-  ( ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) e. _V -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) C_ ( topGen ` ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
54 52 53 syl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) C_ ( topGen ` ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
55 48 54 sstrd 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> T C_ ( topGen ` ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
56 22 12 isfne4 
 |-  ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) <-> ( U. T = U. ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) /\ T C_ ( topGen ` ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) ) )
57 35 55 56 sylanbrc 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y ) /\ ( X = U. T /\ A. x e. S T Fne x ) ) -> T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) )
58 57 ex 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( ( X = U. T /\ A. x e. S T Fne x ) -> T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) ) )
59 32 58 impbid 
 |-  ( ( X e. V /\ A. y e. S X = U. y ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) <-> ( X = U. T /\ A. x e. S T Fne x ) ) )