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 ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → F ↾ 𝑡 A ∈ fBas ⁡ A ↔ ∀ v ∈ F v ∩ A ≠ ∅

Proof

Step Hyp Ref Expression
1 trfbas2 ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → F ↾ 𝑡 A ∈ fBas ⁡ A ↔ ¬ ∅ ∈ F ↾ 𝑡 A
2 elfvdm ⊢ F ∈ fBas ⁡ Y → Y ∈ dom ⁡ fBas
3 ssexg ⊢ A ⊆ Y ∧ Y ∈ dom ⁡ fBas → A ∈ V
4 3 ancoms ⊢ Y ∈ dom ⁡ fBas ∧ A ⊆ Y → A ∈ V
5 2 4 sylan ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → A ∈ V
6 elrest ⊢ F ∈ fBas ⁡ Y ∧ A ∈ V → ∅ ∈ F ↾ 𝑡 A ↔ ∃ v ∈ F ∅ = v ∩ A
7 5 6 syldan ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → ∅ ∈ F ↾ 𝑡 A ↔ ∃ v ∈ F ∅ = v ∩ A
8 7 notbid ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → ¬ ∅ ∈ F ↾ 𝑡 A ↔ ¬ ∃ v ∈ F ∅ = v ∩ A
9 nesym ⊢ v ∩ A ≠ ∅ ↔ ¬ ∅ = v ∩ A
10 9 ralbii ⊢ ∀ v ∈ F v ∩ A ≠ ∅ ↔ ∀ v ∈ F ¬ ∅ = v ∩ A
11 ralnex ⊢ ∀ v ∈ F ¬ ∅ = v ∩ A ↔ ¬ ∃ v ∈ F ∅ = v ∩ A
12 10 11 bitri ⊢ ∀ v ∈ F v ∩ A ≠ ∅ ↔ ¬ ∃ v ∈ F ∅ = v ∩ A
13 8 12 bitr4di ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → ¬ ∅ ∈ F ↾ 𝑡 A ↔ ∀ v ∈ F v ∩ A ≠ ∅
14 1 13 bitrd ⊢ F ∈ fBas ⁡ Y ∧ A ⊆ Y → F ↾ 𝑡 A ∈ fBas ⁡ A ↔ ∀ v ∈ F v ∩ A ≠ ∅