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∈Lv∩A≠∅
2 dfral2 ⊢∀v∈Lv∩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 bitrid ⊢L∈Fil⁡Y∧v∈L→¬v∩A≠∅↔v⊆Y∖A
8 7 rexbidva ⊢L∈Fil⁡Y→∃v∈L¬v∩A≠∅↔∃v∈Lv⊆Y∖A
9 8 adantr ⊢L∈Fil⁡Y∧A⊆Y→∃v∈L¬v∩A≠∅↔∃v∈Lv⊆Y∖A
10 difssd ⊢A⊆Y→Y∖A⊆Y
11 elfilss ⊢L∈Fil⁡Y∧Y∖A⊆Y→Y∖A∈L↔∃v∈Lv⊆Y∖A
12 10 11 sylan2 ⊢L∈Fil⁡Y∧A⊆Y→Y∖A∈L↔∃v∈Lv⊆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 bitrid ⊢L∈Fil⁡Y∧A⊆Y→∀v∈Lv∩A≠∅↔¬Y∖A∈L
16 1 15 bitrd ⊢L∈Fil⁡Y∧A⊆Y→L↾𝑡A∈Fil⁡A↔¬Y∖A∈L