Metamath Proof Explorer

Theorem fgabs

Description: Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion fgabs 
|- ( ( F e. ( fBas ` Y ) /\ Y C_ X ) -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> F e. ( fBas ` Y ) )
2 fgcl 
 |-  ( F e. ( fBas ` Y ) -> ( Y filGen F ) e. ( Fil ` Y ) )
3 filfbas 
 |-  ( ( Y filGen F ) e. ( Fil ` Y ) -> ( Y filGen F ) e. ( fBas ` Y ) )
4 1 2 3 3syl 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( Y filGen F ) e. ( fBas ` Y ) )
5 fbsspw 
 |-  ( ( Y filGen F ) e. ( fBas ` Y ) -> ( Y filGen F ) C_ ~P Y )
6 4 5 syl 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( Y filGen F ) C_ ~P Y )
7 simplr 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> Y C_ X )
8 7 sspwd 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ~P Y C_ ~P X )
9 6 8 sstrd 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( Y filGen F ) C_ ~P X )
10 simpr 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> X e. _V )
11 fbasweak 
 |-  ( ( ( Y filGen F ) e. ( fBas ` Y ) /\ ( Y filGen F ) C_ ~P X /\ X e. _V ) -> ( Y filGen F ) e. ( fBas ` X ) )
12 4 9 10 11 syl3anc 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( Y filGen F ) e. ( fBas ` X ) )
13 elfg 
 |-  ( ( Y filGen F ) e. ( fBas ` X ) -> ( x e. ( X filGen ( Y filGen F ) ) <-> ( x C_ X /\ E. y e. ( Y filGen F ) y C_ x ) ) )
14 12 13 syl 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( x e. ( X filGen ( Y filGen F ) ) <-> ( x C_ X /\ E. y e. ( Y filGen F ) y C_ x ) ) )
15 1 adantr 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ x C_ X ) -> F e. ( fBas ` Y ) )
16 elfg 
 |-  ( F e. ( fBas ` Y ) -> ( y e. ( Y filGen F ) <-> ( y C_ Y /\ E. z e. F z C_ y ) ) )
17 15 16 syl 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ x C_ X ) -> ( y e. ( Y filGen F ) <-> ( y C_ Y /\ E. z e. F z C_ y ) ) )
18 fbsspw 
 |-  ( F e. ( fBas ` Y ) -> F C_ ~P Y )
19 1 18 syl 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> F C_ ~P Y )
20 19 8 sstrd 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> F C_ ~P X )
21 fbasweak 
 |-  ( ( F e. ( fBas ` Y ) /\ F C_ ~P X /\ X e. _V ) -> F e. ( fBas ` X ) )
22 1 20 10 21 syl3anc 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> F e. ( fBas ` X ) )
23 fgcl 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )
24 22 23 syl 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( X filGen F ) e. ( Fil ` X ) )
25 24 ad2antrr 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> ( X filGen F ) e. ( Fil ` X ) )
26 ssfg 
 |-  ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
27 22 26 syl 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> F C_ ( X filGen F ) )
28 27 adantr 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) -> F C_ ( X filGen F ) )
29 28 sselda 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ z e. F ) -> z e. ( X filGen F ) )
30 29 adantrr 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( z e. F /\ z C_ y ) ) -> z e. ( X filGen F ) )
31 30 adantrr 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> z e. ( X filGen F ) )
32 simplrl 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> x C_ X )
33 simprlr 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> z C_ y )
34 simprr 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> y C_ x )
35 33 34 sstrd 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> z C_ x )
36 filss 
 |-  ( ( ( X filGen F ) e. ( Fil ` X ) /\ ( z e. ( X filGen F ) /\ x C_ X /\ z C_ x ) ) -> x e. ( X filGen F ) )
37 25 31 32 35 36 syl13anc 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( ( z e. F /\ z C_ y ) /\ y C_ x ) ) -> x e. ( X filGen F ) )
38 37 expr 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) /\ ( z e. F /\ z C_ y ) ) -> ( y C_ x -> x e. ( X filGen F ) ) )
39 38 rexlimdvaa 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ ( x C_ X /\ y C_ Y ) ) -> ( E. z e. F z C_ y -> ( y C_ x -> x e. ( X filGen F ) ) ) )
40 39 anassrs 
 |-  ( ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ x C_ X ) /\ y C_ Y ) -> ( E. z e. F z C_ y -> ( y C_ x -> x e. ( X filGen F ) ) ) )
41 40 expimpd 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ x C_ X ) -> ( ( y C_ Y /\ E. z e. F z C_ y ) -> ( y C_ x -> x e. ( X filGen F ) ) ) )
42 17 41 sylbid 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ x C_ X ) -> ( y e. ( Y filGen F ) -> ( y C_ x -> x e. ( X filGen F ) ) ) )
43 42 rexlimdv 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) /\ x C_ X ) -> ( E. y e. ( Y filGen F ) y C_ x -> x e. ( X filGen F ) ) )
44 43 expimpd 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( ( x C_ X /\ E. y e. ( Y filGen F ) y C_ x ) -> x e. ( X filGen F ) ) )
45 14 44 sylbid 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( x e. ( X filGen ( Y filGen F ) ) -> x e. ( X filGen F ) ) )
46 45 ssrdv 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( X filGen ( Y filGen F ) ) C_ ( X filGen F ) )
47 ssfg 
 |-  ( F e. ( fBas ` Y ) -> F C_ ( Y filGen F ) )
48 47 ad2antrr 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> F C_ ( Y filGen F ) )
49 fgss 
 |-  ( ( F e. ( fBas ` X ) /\ ( Y filGen F ) e. ( fBas ` X ) /\ F C_ ( Y filGen F ) ) -> ( X filGen F ) C_ ( X filGen ( Y filGen F ) ) )
50 22 12 48 49 syl3anc 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( X filGen F ) C_ ( X filGen ( Y filGen F ) ) )
51 46 50 eqssd 
 |-  ( ( ( F e. ( fBas ` Y ) /\ Y C_ X ) /\ X e. _V ) -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )
52 51 ex 
 |-  ( ( F e. ( fBas ` Y ) /\ Y C_ X ) -> ( X e. _V -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) ) )
53 df-fg 
 |-  filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
54 53 reldmmpo 
 |-  Rel dom filGen
55 54 ovprc1 
 |-  ( -. X e. _V -> ( X filGen ( Y filGen F ) ) = (/) )
56 54 ovprc1 
 |-  ( -. X e. _V -> ( X filGen F ) = (/) )
57 55 56 eqtr4d 
 |-  ( -. X e. _V -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )
58 52 57 pm2.61d1 
 |-  ( ( F e. ( fBas ` Y ) /\ Y C_ X ) -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )