Metamath Proof Explorer

Theorem trfil3

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

Ref Expression
Assertion trfil3 ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → L ↾ 𝑡 A ∈ Fil ⁡ A ↔ ¬ Y ∖ A ∈ L

Proof

Step Hyp Ref Expression
1 trfil2 ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → L ↾ 𝑡 A ∈ Fil ⁡ A ↔ ∀ v ∈ L v ∩ A ≠ ∅
2 dfral2 ⊢ ∀ v ∈ L v ∩ A ≠ ∅ ↔ ¬ ∃ v ∈ L ¬ v ∩ A ≠ ∅
3 nne ⊢ ¬ v ∩ A ≠ ∅ ↔ v ∩ A = ∅
4 filelss ⊢ L ∈ Fil ⁡ Y ∧ v ∈ L → v ⊆ Y
5 reldisj ⊢ v ⊆ Y → v ∩ A = ∅ ↔ v ⊆ Y ∖ A
6 4 5 syl ⊢ L ∈ Fil ⁡ Y ∧ v ∈ L → v ∩ A = ∅ ↔ v ⊆ Y ∖ A
7 3 6 syl5bb ⊢ L ∈ Fil ⁡ Y ∧ v ∈ L → ¬ v ∩ A ≠ ∅ ↔ v ⊆ Y ∖ A
8 7 rexbidva ⊢ L ∈ Fil ⁡ Y → ∃ v ∈ L ¬ v ∩ A ≠ ∅ ↔ ∃ v ∈ L v ⊆ Y ∖ A
9 8 adantr ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → ∃ v ∈ L ¬ v ∩ A ≠ ∅ ↔ ∃ v ∈ L v ⊆ Y ∖ A
10 difssd ⊢ A ⊆ Y → Y ∖ A ⊆ Y
11 elfilss ⊢ L ∈ Fil ⁡ Y ∧ Y ∖ A ⊆ Y → Y ∖ A ∈ L ↔ ∃ v ∈ L v ⊆ Y ∖ A
12 10 11 sylan2 ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → Y ∖ A ∈ L ↔ ∃ v ∈ L v ⊆ Y ∖ A
13 9 12 bitr4d ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → ∃ v ∈ L ¬ v ∩ A ≠ ∅ ↔ Y ∖ A ∈ L
14 13 notbid ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → ¬ ∃ v ∈ L ¬ v ∩ A ≠ ∅ ↔ ¬ Y ∖ A ∈ L
15 2 14 syl5bb ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → ∀ v ∈ L v ∩ A ≠ ∅ ↔ ¬ Y ∖ A ∈ L
16 1 15 bitrd ⊢ L ∈ Fil ⁡ Y ∧ A ⊆ Y → L ↾ 𝑡 A ∈ Fil ⁡ A ↔ ¬ Y ∖ A ∈ L