Theorem isfbas2

Description: The predicate " F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	isfbas2	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfbas	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
2		elin	⊢ ( 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
3		velpw	⊢ ( 𝑧 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ↔ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
4	3	anbi2i	⊢ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
5	2 4	bitri	⊢ ( 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6	5	exbii	⊢ ( ∃ 𝑧 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
7		n0	⊢ ( ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
8		df-rex	⊢ ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
9	6 7 8	3bitr4i	⊢ ( ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
10	9	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
11	10	3anbi3i	⊢ ( ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
12	11	anbi2i	⊢ ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
13	1 12	bitrdi	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )