Step |
Hyp |
Ref |
Expression |
1 |
|
pwexg |
⊢ ( 𝐵 ∈ 𝐴 → 𝒫 𝐵 ∈ V ) |
2 |
|
elpw2g |
⊢ ( 𝒫 𝐵 ∈ V → ( 𝐹 ∈ 𝒫 𝒫 𝐵 ↔ 𝐹 ⊆ 𝒫 𝐵 ) ) |
3 |
1 2
|
syl |
⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ 𝒫 𝒫 𝐵 ↔ 𝐹 ⊆ 𝒫 𝐵 ) ) |
4 |
3
|
anbi1d |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) |
5 |
|
elex |
⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ V ) |
6 |
5
|
biantrurd |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) ) |
7 |
4 6
|
bitr3d |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) ) |
8 |
|
df-fbas |
⊢ fBas = ( 𝑧 ∈ V ↦ { 𝑤 ∈ 𝒫 𝒫 𝑧 ∣ ( 𝑤 ≠ ∅ ∧ ∅ ∉ 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) } ) |
9 |
|
neeq1 |
⊢ ( 𝑤 = 𝐹 → ( 𝑤 ≠ ∅ ↔ 𝐹 ≠ ∅ ) ) |
10 |
|
neleq2 |
⊢ ( 𝑤 = 𝐹 → ( ∅ ∉ 𝑤 ↔ ∅ ∉ 𝐹 ) ) |
11 |
|
ineq1 |
⊢ ( 𝑤 = 𝐹 → ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
12 |
11
|
neeq1d |
⊢ ( 𝑤 = 𝐹 → ( ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) |
13 |
12
|
raleqbi1dv |
⊢ ( 𝑤 = 𝐹 → ( ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) |
14 |
13
|
raleqbi1dv |
⊢ ( 𝑤 = 𝐹 → ( ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) |
15 |
9 10 14
|
3anbi123d |
⊢ ( 𝑤 = 𝐹 → ( ( 𝑤 ≠ ∅ ∧ ∅ ∉ 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) |
16 |
15
|
adantl |
⊢ ( ( 𝑧 = 𝐵 ∧ 𝑤 = 𝐹 ) → ( ( 𝑤 ≠ ∅ ∧ ∅ ∉ 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) |
17 |
|
pweq |
⊢ ( 𝑧 = 𝐵 → 𝒫 𝑧 = 𝒫 𝐵 ) |
18 |
17
|
pweqd |
⊢ ( 𝑧 = 𝐵 → 𝒫 𝒫 𝑧 = 𝒫 𝒫 𝐵 ) |
19 |
|
vpwex |
⊢ 𝒫 𝑧 ∈ V |
20 |
19
|
pwex |
⊢ 𝒫 𝒫 𝑧 ∈ V |
21 |
20
|
a1i |
⊢ ( 𝑧 ∈ V → 𝒫 𝒫 𝑧 ∈ V ) |
22 |
8 16 18 21
|
elmptrab |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐵 ∈ V ∧ 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) |
23 |
|
3anass |
⊢ ( ( 𝐵 ∈ V ∧ 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) |
24 |
22 23
|
bitri |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) |
25 |
7 24
|
syl6rbbr |
⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) |