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 ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ 𝐹 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )