Metamath Proof Explorer

Theorem fgss2

Description: A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fgss2 
|- ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( X filGen F ) C_ ( X filGen G ) <-> A. x e. F E. y e. G y C_ x ) )

Proof

Step Hyp Ref Expression
1 ssfg 
 |-  ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
2 1 adantr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> F C_ ( X filGen F ) )
3 2 sseld 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( x e. F -> x e. ( X filGen F ) ) )
4 ssel2 
 |-  ( ( ( X filGen F ) C_ ( X filGen G ) /\ x e. ( X filGen F ) ) -> x e. ( X filGen G ) )
5 elfg 
 |-  ( G e. ( fBas ` X ) -> ( x e. ( X filGen G ) <-> ( x C_ X /\ E. y e. G y C_ x ) ) )
6 simpr 
 |-  ( ( x C_ X /\ E. y e. G y C_ x ) -> E. y e. G y C_ x )
7 5 6 syl6bi 
 |-  ( G e. ( fBas ` X ) -> ( x e. ( X filGen G ) -> E. y e. G y C_ x ) )
8 7 adantl 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( x e. ( X filGen G ) -> E. y e. G y C_ x ) )
9 4 8 syl5 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( ( X filGen F ) C_ ( X filGen G ) /\ x e. ( X filGen F ) ) -> E. y e. G y C_ x ) )
10 9 expd 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( X filGen F ) C_ ( X filGen G ) -> ( x e. ( X filGen F ) -> E. y e. G y C_ x ) ) )
11 3 10 syl5d 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( X filGen F ) C_ ( X filGen G ) -> ( x e. F -> E. y e. G y C_ x ) ) )
12 11 ralrimdv 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( X filGen F ) C_ ( X filGen G ) -> A. x e. F E. y e. G y C_ x ) )
13 sseq2 
 |-  ( x = u -> ( y C_ x <-> y C_ u ) )
14 13 rexbidv 
 |-  ( x = u -> ( E. y e. G y C_ x <-> E. y e. G y C_ u ) )
15 14 rspcv 
 |-  ( u e. F -> ( A. x e. F E. y e. G y C_ x -> E. y e. G y C_ u ) )
16 15 adantl 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) -> ( A. x e. F E. y e. G y C_ x -> E. y e. G y C_ u ) )
17 sstr 
 |-  ( ( y C_ u /\ u C_ t ) -> y C_ t )
18 sseq1 
 |-  ( v = y -> ( v C_ t <-> y C_ t ) )
19 18 rspcev 
 |-  ( ( y e. G /\ y C_ t ) -> E. v e. G v C_ t )
20 19 adantl 
 |-  ( ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) /\ ( y e. G /\ y C_ t ) ) -> E. v e. G v C_ t )
21 20 a1d 
 |-  ( ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) /\ ( y e. G /\ y C_ t ) ) -> ( t C_ X -> E. v e. G v C_ t ) )
22 17 21 sylanr2 
 |-  ( ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) /\ ( y e. G /\ ( y C_ u /\ u C_ t ) ) ) -> ( t C_ X -> E. v e. G v C_ t ) )
23 22 ancld 
 |-  ( ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) /\ ( y e. G /\ ( y C_ u /\ u C_ t ) ) ) -> ( t C_ X -> ( t C_ X /\ E. v e. G v C_ t ) ) )
24 23 exp45 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) -> ( y e. G -> ( y C_ u -> ( u C_ t -> ( t C_ X -> ( t C_ X /\ E. v e. G v C_ t ) ) ) ) ) )
25 24 rexlimdv 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) -> ( E. y e. G y C_ u -> ( u C_ t -> ( t C_ X -> ( t C_ X /\ E. v e. G v C_ t ) ) ) ) )
26 16 25 syld 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ u e. F ) -> ( A. x e. F E. y e. G y C_ x -> ( u C_ t -> ( t C_ X -> ( t C_ X /\ E. v e. G v C_ t ) ) ) ) )
27 26 impancom 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( u e. F -> ( u C_ t -> ( t C_ X -> ( t C_ X /\ E. v e. G v C_ t ) ) ) ) )
28 27 rexlimdv 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( E. u e. F u C_ t -> ( t C_ X -> ( t C_ X /\ E. v e. G v C_ t ) ) ) )
29 28 impcomd 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( ( t C_ X /\ E. u e. F u C_ t ) -> ( t C_ X /\ E. v e. G v C_ t ) ) )
30 elfg 
 |-  ( F e. ( fBas ` X ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. u e. F u C_ t ) ) )
31 30 adantr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. u e. F u C_ t ) ) )
32 31 adantr 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. u e. F u C_ t ) ) )
33 elfg 
 |-  ( G e. ( fBas ` X ) -> ( t e. ( X filGen G ) <-> ( t C_ X /\ E. v e. G v C_ t ) ) )
34 33 adantl 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( t e. ( X filGen G ) <-> ( t C_ X /\ E. v e. G v C_ t ) ) )
35 34 adantr 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( t e. ( X filGen G ) <-> ( t C_ X /\ E. v e. G v C_ t ) ) )
36 29 32 35 3imtr4d 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( t e. ( X filGen F ) -> t e. ( X filGen G ) ) )
37 36 ssrdv 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) /\ A. x e. F E. y e. G y C_ x ) -> ( X filGen F ) C_ ( X filGen G ) )
38 37 ex 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F E. y e. G y C_ x -> ( X filGen F ) C_ ( X filGen G ) ) )
39 12 38 impbid 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( X filGen F ) C_ ( X filGen G ) <-> A. x e. F E. y e. G y C_ x ) )