# 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 ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({L}{↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)↔¬{Y}\setminus {A}\in {L}\right)$

### Proof

Step Hyp Ref Expression
1 trfil2 ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({L}{↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)↔\forall {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\cap {A}\ne \varnothing \right)$
2 dfral2 ${⊢}\forall {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\cap {A}\ne \varnothing ↔¬\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}¬{v}\cap {A}\ne \varnothing$
3 nne ${⊢}¬{v}\cap {A}\ne \varnothing ↔{v}\cap {A}=\varnothing$
4 filelss ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {v}\in {L}\right)\to {v}\subseteq {Y}$
5 reldisj ${⊢}{v}\subseteq {Y}\to \left({v}\cap {A}=\varnothing ↔{v}\subseteq {Y}\setminus {A}\right)$
6 4 5 syl ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {v}\in {L}\right)\to \left({v}\cap {A}=\varnothing ↔{v}\subseteq {Y}\setminus {A}\right)$
7 3 6 syl5bb ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {v}\in {L}\right)\to \left(¬{v}\cap {A}\ne \varnothing ↔{v}\subseteq {Y}\setminus {A}\right)$
8 7 rexbidva ${⊢}{L}\in \mathrm{Fil}\left({Y}\right)\to \left(\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}¬{v}\cap {A}\ne \varnothing ↔\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\subseteq {Y}\setminus {A}\right)$
9 8 adantr ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left(\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}¬{v}\cap {A}\ne \varnothing ↔\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\subseteq {Y}\setminus {A}\right)$
10 difssd ${⊢}{A}\subseteq {Y}\to {Y}\setminus {A}\subseteq {Y}$
11 elfilss ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {Y}\setminus {A}\subseteq {Y}\right)\to \left({Y}\setminus {A}\in {L}↔\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\subseteq {Y}\setminus {A}\right)$
12 10 11 sylan2 ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({Y}\setminus {A}\in {L}↔\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\subseteq {Y}\setminus {A}\right)$
13 9 12 bitr4d ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left(\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}¬{v}\cap {A}\ne \varnothing ↔{Y}\setminus {A}\in {L}\right)$
14 13 notbid ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left(¬\exists {v}\in {L}\phantom{\rule{.4em}{0ex}}¬{v}\cap {A}\ne \varnothing ↔¬{Y}\setminus {A}\in {L}\right)$
15 2 14 syl5bb ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left(\forall {v}\in {L}\phantom{\rule{.4em}{0ex}}{v}\cap {A}\ne \varnothing ↔¬{Y}\setminus {A}\in {L}\right)$
16 1 15 bitrd ${⊢}\left({L}\in \mathrm{Fil}\left({Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({L}{↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)↔¬{Y}\setminus {A}\in {L}\right)$