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 ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A = ⋃ L ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 sseqin2 ⊢ A ⊆ Y ↔ Y ∩ A = A
2 1 bilani ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∩ A = A
3 simpl ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → L ∈ Fil ⁡ Y
4 id ⊢ A ⊆ Y → A ⊆ Y
5 filtop ⊢ L ∈ Fil ⁡ Y → Y ∈ L
6 ssexg ⊢ A ⊆ Y ∧ Y ∈ L → A ∈ V
7 4 5 6 syl2anr ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ∈ V
8 5 adantr ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∈ L
9 elrestr ⊢ L ∈ Fil ⁡ Y ∧ A ∈ V ∧ Y ∈ L → Y ∩ A ∈ L ↾ 𝑡 A
10 3 7 8 9 syl3anc ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∩ A ∈ L ↾ 𝑡 A
11 2 10 eqeltrrd ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ∈ L ↾ 𝑡 A
12 elssuni ⊢ A ∈ L ↾ 𝑡 A → A ⊆ ⋃ L ↾ 𝑡 A
13 11 12 syl ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ⊆ ⋃ L ↾ 𝑡 A
14 restsspw ⊢ L ↾ 𝑡 A ⊆ 𝒫 A
15 sspwuni ⊢ L ↾ 𝑡 A ⊆ 𝒫 A ↔ ⋃ L ↾ 𝑡 A ⊆ A
16 14 15 mpbi ⊢ ⋃ L ↾ 𝑡 A ⊆ A
17 16 a1i ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → ⋃ L ↾ 𝑡 A ⊆ A
18 13 17 eqssd ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A = ⋃ L ↾ 𝑡 A