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