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 sseqin2 ⊢ ( 𝐴 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝐴 ) = 𝐴 )
2 1 bilani ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) = 𝐴 )
3 simpl ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
4 id ⊢ ( 𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌 )
5 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝐿 )
6 ssexg ⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿 ) → 𝐴 ∈ V )
7 4 5 6 syl2anr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
8 5 adantr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝑌 ∈ 𝐿 )
9 elrestr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
10 3 7 8 9 syl3anc ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
11 2 10 eqeltrrd ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) )
12 elssuni ⊢ ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) → 𝐴 ⊆ ∪ ( 𝐿 ↾t 𝐴 ) )
13 11 12 syl ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ⊆ ∪ ( 𝐿 ↾t 𝐴 ) )
14 restsspw ⊢ ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴
15 sspwuni ⊢ ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴 )
16 14 15 mpbi ⊢ ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴
17 16 a1i ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴 )
18 13 17 eqssd ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 = ∪ ( 𝐿 ↾t 𝐴 ) )