This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fgtr

Description: If A is a member of the filter, then truncating F to A and regenerating the behavior outside A using filGen recovers the original filter. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion fgtr 
|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( X filGen ( F |`t A ) ) = F )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2 fbncp 
 |-  ( ( F e. ( fBas ` X ) /\ A e. F ) -> -. ( X \ A ) e. F )
3 1 2 sylan 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> -. ( X \ A ) e. F )
4 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> A C_ X )
5 trfil3 
 |-  ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( ( F |`t A ) e. ( Fil ` A ) <-> -. ( X \ A ) e. F ) )
6 4 5 syldan 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( ( F |`t A ) e. ( Fil ` A ) <-> -. ( X \ A ) e. F ) )
7 3 6 mpbird 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) e. ( Fil ` A ) )
8 filfbas 
 |-  ( ( F |`t A ) e. ( Fil ` A ) -> ( F |`t A ) e. ( fBas ` A ) )
9 7 8 syl 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) e. ( fBas ` A ) )
10 restsspw 
 |-  ( F |`t A ) C_ ~P A
11 4 sspwd 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ~P A C_ ~P X )
12 10 11 sstrid 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) C_ ~P X )
13 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
14 13 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> X e. F )
15 fbasweak 
 |-  ( ( ( F |`t A ) e. ( fBas ` A ) /\ ( F |`t A ) C_ ~P X /\ X e. F ) -> ( F |`t A ) e. ( fBas ` X ) )
16 9 12 14 15 syl3anc 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) e. ( fBas ` X ) )
17 1 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> F e. ( fBas ` X ) )
18 trfilss 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) C_ F )
19 fgss 
 |-  ( ( ( F |`t A ) e. ( fBas ` X ) /\ F e. ( fBas ` X ) /\ ( F |`t A ) C_ F ) -> ( X filGen ( F |`t A ) ) C_ ( X filGen F ) )
20 16 17 18 19 syl3anc 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( X filGen ( F |`t A ) ) C_ ( X filGen F ) )
21 fgfil 
 |-  ( F e. ( Fil ` X ) -> ( X filGen F ) = F )
22 21 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( X filGen F ) = F )
23 20 22 sseqtrd 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( X filGen ( F |`t A ) ) C_ F )
24 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ x e. F ) -> x C_ X )
25 24 ex 
 |-  ( F e. ( Fil ` X ) -> ( x e. F -> x C_ X ) )
26 25 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( x e. F -> x C_ X ) )
27 elrestr 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F /\ x e. F ) -> ( x i^i A ) e. ( F |`t A ) )
28 27 3expa 
 |-  ( ( ( F e. ( Fil ` X ) /\ A e. F ) /\ x e. F ) -> ( x i^i A ) e. ( F |`t A ) )
29 inss1 
 |-  ( x i^i A ) C_ x
30 sseq1 
 |-  ( y = ( x i^i A ) -> ( y C_ x <-> ( x i^i A ) C_ x ) )
31 30 rspcev 
 |-  ( ( ( x i^i A ) e. ( F |`t A ) /\ ( x i^i A ) C_ x ) -> E. y e. ( F |`t A ) y C_ x )
32 28 29 31 sylancl 
 |-  ( ( ( F e. ( Fil ` X ) /\ A e. F ) /\ x e. F ) -> E. y e. ( F |`t A ) y C_ x )
33 32 ex 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( x e. F -> E. y e. ( F |`t A ) y C_ x ) )
34 26 33 jcad 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( x e. F -> ( x C_ X /\ E. y e. ( F |`t A ) y C_ x ) ) )
35 elfg 
 |-  ( ( F |`t A ) e. ( fBas ` X ) -> ( x e. ( X filGen ( F |`t A ) ) <-> ( x C_ X /\ E. y e. ( F |`t A ) y C_ x ) ) )
36 16 35 syl 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( x e. ( X filGen ( F |`t A ) ) <-> ( x C_ X /\ E. y e. ( F |`t A ) y C_ x ) ) )
37 34 36 sylibrd 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( x e. F -> x e. ( X filGen ( F |`t A ) ) ) )
38 37 ssrdv 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> F C_ ( X filGen ( F |`t A ) ) )
39 23 38 eqssd 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( X filGen ( F |`t A ) ) = F )