Metamath Proof Explorer


Theorem trfbas

Description: Conditions for the trace of a filter base F to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion trfbas FfBasYAYF𝑡AfBasAvFvA

Proof

Step Hyp Ref Expression
1 trfbas2 FfBasYAYF𝑡AfBasA¬F𝑡A
2 elfvdm FfBasYYdomfBas
3 ssexg AYYdomfBasAV
4 3 ancoms YdomfBasAYAV
5 2 4 sylan FfBasYAYAV
6 elrest FfBasYAVF𝑡AvF=vA
7 5 6 syldan FfBasYAYF𝑡AvF=vA
8 7 notbid FfBasYAY¬F𝑡A¬vF=vA
9 nesym vA¬=vA
10 9 ralbii vFvAvF¬=vA
11 ralnex vF¬=vA¬vF=vA
12 10 11 bitri vFvA¬vF=vA
13 8 12 bitr4di FfBasYAY¬F𝑡AvFvA
14 1 13 bitrd FfBasYAYF𝑡AfBasAvFvA