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 simpr ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ⊆ Y
2 sseqin2 ⊢ A ⊆ Y ↔ Y ∩ A = A
3 1 2 sylib ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∩ A = A
4 simpl ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → L ∈ Fil ⁡ Y
5 id ⊢ A ⊆ Y → A ⊆ Y
6 filtop ⊢ L ∈ Fil ⁡ Y → Y ∈ L
7 ssexg ⊢ A ⊆ Y ∧ Y ∈ L → A ∈ V
8 5 6 7 syl2anr ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ∈ V
9 6 adantr ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∈ L
10 elrestr ⊢ L ∈ Fil ⁡ Y ∧ A ∈ V ∧ Y ∈ L → Y ∩ A ∈ L ↾ 𝑡 A
11 4 8 9 10 syl3anc ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∩ A ∈ L ↾ 𝑡 A
12 3 11 eqeltrrd ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ∈ L ↾ 𝑡 A
13 elssuni ⊢ A ∈ L ↾ 𝑡 A → A ⊆ ⋃ L ↾ 𝑡 A
14 12 13 syl ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A ⊆ ⋃ L ↾ 𝑡 A
15 restsspw ⊢ L ↾ 𝑡 A ⊆ 𝒫 A
16 sspwuni ⊢ L ↾ 𝑡 A ⊆ 𝒫 A ↔ ⋃ L ↾ 𝑡 A ⊆ A
17 15 16 mpbi ⊢ ⋃ L ↾ 𝑡 A ⊆ A
18 17 a1i ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → ⋃ L ↾ 𝑡 A ⊆ A
19 14 18 eqssd ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → A = ⋃ L ↾ 𝑡 A