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 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2 fbncp ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝐴 ) ∈ 𝐹 )
3 1 2 sylan ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝐴 ) ∈ 𝐹 )
4 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ 𝑋 )
5 trfil3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑋 ∖ 𝐴 ) ∈ 𝐹 ) )
6 4 5 syldan ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑋 ∖ 𝐴 ) ∈ 𝐹 ) )
7 3 6 mpbird ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
8 filfbas ⊢ ( ( 𝐹 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
9 7 8 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
10 restsspw ⊢ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴
11 sspwb ⊢ ( 𝐴 ⊆ 𝑋 ↔ 𝒫 𝐴 ⊆ 𝒫 𝑋 )
12 4 11 sylib ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝒫 𝐴 ⊆ 𝒫 𝑋 )
13 10 12 sstrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝑋 )
14 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
15 14 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝑋 ∈ 𝐹 )
16 fbasweak ⊢ ( ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) )
17 9 13 15 16 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) )
18 1 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
19 trfilss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝐹 )
20 fgss ⊢ ( ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ⊆ ( 𝑋 filGen 𝐹 ) )
21 17 18 19 20 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ⊆ ( 𝑋 filGen 𝐹 ) )
22 fgfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
24 21 23 sseqtrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ⊆ 𝐹 )
25 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝑋 )
26 25 ex ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ 𝑋 ) )
27 26 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ 𝑋 ) )
28 elrestr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
29 28 3expa ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
30 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
31 sseq1 ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐴 ) → ( 𝑦 ⊆ 𝑥 ↔ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) )
32 31 rspcev ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 )
33 29 30 32 sylancl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 )
34 33 ex ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) )
35 27 34 jcad ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) ) )
36 elfg ⊢ ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) ) )
37 17 36 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) ) )
38 35 37 sylibrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ∈ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ) )
39 38 ssrdv ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐹 ⊆ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) )
40 24 39 eqssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) = 𝐹 )