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

Metamath Proof Explorer

Theorem trfil1

Description: Conditions for the trace of a filter L to be a filter. (Contributed by FL, 2-Sep-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion trfil1 ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 = ∪ ( 𝐿 ↾t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ⊆ 𝑌 )
2 sseqin2 ⊢ ( 𝐴 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝐴 ) = 𝐴 )
3 1 2 sylib ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) = 𝐴 )
4 simpl ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
5 id ⊢ ( 𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌 )
6 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝐿 )
7 ssexg ⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿 ) → 𝐴 ∈ V )
8 5 6 7 syl2anr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
9 6 adantr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝑌 ∈ 𝐿 )
10 elrestr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
11 4 8 9 10 syl3anc ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
12 3 11 eqeltrrd ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) )
13 elssuni ⊢ ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) → 𝐴 ⊆ ∪ ( 𝐿 ↾t 𝐴 ) )
14 12 13 syl ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ⊆ ∪ ( 𝐿 ↾t 𝐴 ) )
15 restsspw ⊢ ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴
16 sspwuni ⊢ ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴 )
17 15 16 mpbi ⊢ ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴
18 17 a1i ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴 )
19 14 18 eqssd ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 = ∪ ( 𝐿 ↾t 𝐴 ) )