Metamath Proof Explorer

Theorem fnemeet1

Description: The meet of a collection of equivalence classes of covers with respect to fineness. (Contributed by Jeff Hankins, 5-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 unitg 
 |-  ( t e. S -> U. ( topGen ` t ) = U. t )
2 1 adantl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> U. ( topGen ` t ) = U. t )
3 unieq 
 |-  ( y = t -> U. y = U. t )
4 3 eqeq2d 
 |-  ( y = t -> ( X = U. y <-> X = U. t ) )
5 4 rspccva 
 |-  ( ( A. y e. S X = U. y /\ t e. S ) -> X = U. t )
6 5 3ad2antl2 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> X = U. t )
7 2 6 eqtr4d 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> U. ( topGen ` t ) = X )
8 eqimss 
 |-  ( U. ( topGen ` t ) = X -> U. ( topGen ` t ) C_ X )
9 7 8 syl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> U. ( topGen ` t ) C_ X )
10 sspwuni 
 |-  ( ( topGen ` t ) C_ ~P X <-> U. ( topGen ` t ) C_ X )
11 9 10 sylibr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> ( topGen ` t ) C_ ~P X )
12 11 ralrimiva 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A. t e. S ( topGen ` t ) C_ ~P X )
13 ne0i 
 |-  ( A e. S -> S =/= (/) )
14 13 3ad2ant3 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> S =/= (/) )
15 riinn0 
 |-  ( ( A. t e. S ( topGen ` t ) C_ ~P X /\ S =/= (/) ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = |^|_ t e. S ( topGen ` t ) )
16 12 14 15 syl2anc 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) = |^|_ t e. S ( topGen ` t ) )
17 simp3 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A e. S )
18 ssid 
 |-  ( topGen ` A ) C_ ( topGen ` A )
19 fveq2 
 |-  ( t = A -> ( topGen ` t ) = ( topGen ` A ) )
20 19 sseq1d 
 |-  ( t = A -> ( ( topGen ` t ) C_ ( topGen ` A ) <-> ( topGen ` A ) C_ ( topGen ` A ) ) )
21 20 rspcev 
 |-  ( ( A e. S /\ ( topGen ` A ) C_ ( topGen ` A ) ) -> E. t e. S ( topGen ` t ) C_ ( topGen ` A ) )
22 17 18 21 sylancl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> E. t e. S ( topGen ` t ) C_ ( topGen ` A ) )
23 iinss 
 |-  ( E. t e. S ( topGen ` t ) C_ ( topGen ` A ) -> |^|_ t e. S ( topGen ` t ) C_ ( topGen ` A ) )
24 22 23 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> |^|_ t e. S ( topGen ` t ) C_ ( topGen ` A ) )
25 24 unissd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. |^|_ t e. S ( topGen ` t ) C_ U. ( topGen ` A ) )
26 unitg 
 |-  ( A e. S -> U. ( topGen ` A ) = U. A )
27 26 3ad2ant3 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. ( topGen ` A ) = U. A )
28 25 27 sseqtrd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. |^|_ t e. S ( topGen ` t ) C_ U. A )
29 unieq 
 |-  ( y = A -> U. y = U. A )
30 29 eqeq2d 
 |-  ( y = A -> ( X = U. y <-> X = U. A ) )
31 30 rspccva 
 |-  ( ( A. y e. S X = U. y /\ A e. S ) -> X = U. A )
32 31 3adant1 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> X = U. A )
33 32 adantr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> X = U. A )
34 33 6 eqtr3d 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> U. A = U. t )
35 simpr 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> t e. S )
36 ssid 
 |-  t C_ t
37 eltg3i 
 |-  ( ( t e. S /\ t C_ t ) -> U. t e. ( topGen ` t ) )
38 35 36 37 sylancl 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> U. t e. ( topGen ` t ) )
39 34 38 eqeltrd 
 |-  ( ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) /\ t e. S ) -> U. A e. ( topGen ` t ) )
40 39 ralrimiva 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A. t e. S U. A e. ( topGen ` t ) )
41 uniexg 
 |-  ( A e. S -> U. A e. _V )
42 41 3ad2ant3 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. A e. _V )
43 eliin 
 |-  ( U. A e. _V -> ( U. A e. |^|_ t e. S ( topGen ` t ) <-> A. t e. S U. A e. ( topGen ` t ) ) )
44 42 43 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> ( U. A e. |^|_ t e. S ( topGen ` t ) <-> A. t e. S U. A e. ( topGen ` t ) ) )
45 40 44 mpbird 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. A e. |^|_ t e. S ( topGen ` t ) )
46 elssuni 
 |-  ( U. A e. |^|_ t e. S ( topGen ` t ) -> U. A C_ U. |^|_ t e. S ( topGen ` t ) )
47 45 46 syl 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. A C_ U. |^|_ t e. S ( topGen ` t ) )
48 28 47 eqssd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> U. |^|_ t e. S ( topGen ` t ) = U. A )
49 eqid 
 |-  U. |^|_ t e. S ( topGen ` t ) = U. |^|_ t e. S ( topGen ` t )
50 eqid 
 |-  U. A = U. A
51 49 50 isfne4 
 |-  ( |^|_ t e. S ( topGen ` t ) Fne A <-> ( U. |^|_ t e. S ( topGen ` t ) = U. A /\ |^|_ t e. S ( topGen ` t ) C_ ( topGen ` A ) ) )
52 48 24 51 sylanbrc 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> |^|_ t e. S ( topGen ` t ) Fne A )
53 16 52 eqbrtrd 
 |-  ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) Fne A )