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 ( ( 𝐹 ∈ ( 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 4 sspwd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝒫 𝐴 ⊆ 𝒫 𝑋 )
12 10 11 sstrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝑋 )
13 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
14 13 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝑋 ∈ 𝐹 )
15 fbasweak ⊢ ( ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) )
16 9 12 14 15 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) )
17 1 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
18 trfilss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝐹 )
19 fgss ⊢ ( ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ⊆ ( 𝑋 filGen 𝐹 ) )
20 16 17 18 19 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ⊆ ( 𝑋 filGen 𝐹 ) )
21 fgfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
22 21 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
23 20 22 sseqtrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ⊆ 𝐹 )
24 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝑋 )
25 24 ex ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ 𝑋 ) )
26 25 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ 𝑋 ) )
27 elrestr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
28 27 3expa ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
29 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
30 sseq1 ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐴 ) → ( 𝑦 ⊆ 𝑥 ↔ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) )
31 30 rspcev ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 )
32 28 29 31 sylancl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 )
33 32 ex ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) )
34 26 33 jcad ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) ) )
35 elfg ⊢ ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) ) )
36 16 35 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ) ) )
37 34 36 sylibrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ∈ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) ) )
38 37 ssrdv ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐹 ⊆ ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) )
39 23 38 eqssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝐴 ) ) = 𝐹 )