This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ 𝐹 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 trfbas2 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) )
2 elfvdm ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas )
3 ssexg ⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ dom fBas ) → 𝐴 ∈ V )
4 3 ancoms ⊢ ( ( 𝑌 ∈ dom fBas ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
5 2 4 sylan ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
6 elrest ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( ∅ ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐹 ∅ = ( 𝑣 ∩ 𝐴 ) ) )
7 5 6 syldan ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∅ ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐹 ∅ = ( 𝑣 ∩ 𝐴 ) ) )
8 7 notbid ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ↔ ¬ ∃ 𝑣 ∈ 𝐹 ∅ = ( 𝑣 ∩ 𝐴 ) ) )
9 nesym ⊢ ( ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ∅ = ( 𝑣 ∩ 𝐴 ) )
10 9 ralbii ⊢ ( ∀ 𝑣 ∈ 𝐹 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝐹 ¬ ∅ = ( 𝑣 ∩ 𝐴 ) )
11 ralnex ⊢ ( ∀ 𝑣 ∈ 𝐹 ¬ ∅ = ( 𝑣 ∩ 𝐴 ) ↔ ¬ ∃ 𝑣 ∈ 𝐹 ∅ = ( 𝑣 ∩ 𝐴 ) )
12 10 11 bitri ⊢ ( ∀ 𝑣 ∈ 𝐹 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ∃ 𝑣 ∈ 𝐹 ∅ = ( 𝑣 ∩ 𝐴 ) )
13 8 12 bitr4di ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∀ 𝑣 ∈ 𝐹 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )
14 1 13 bitrd ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ 𝐹 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )