Step |
Hyp |
Ref |
Expression |
1 |
|
elfvdm |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐵 ∈ dom fBas ) |
2 |
|
isfbas |
⊢ ( 𝐵 ∈ dom fBas → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) |
3 |
1 2
|
syl |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) |
4 |
3
|
ibi |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) |
5 |
|
simpr1 |
⊢ ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) → 𝐹 ≠ ∅ ) |
6 |
4 5
|
syl |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐹 ≠ ∅ ) |