Step |
Hyp |
Ref |
Expression |
1 |
|
df-fil |
⊢ Fil = ( 𝑧 ∈ V ↦ { 𝑓 ∈ ( fBas ‘ 𝑧 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑧 ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝑓 ) } ) |
2 |
|
pweq |
⊢ ( 𝑧 = 𝑋 → 𝒫 𝑧 = 𝒫 𝑋 ) |
3 |
2
|
adantr |
⊢ ( ( 𝑧 = 𝑋 ∧ 𝑓 = 𝐹 ) → 𝒫 𝑧 = 𝒫 𝑋 ) |
4 |
|
ineq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∩ 𝒫 𝑥 ) = ( 𝐹 ∩ 𝒫 𝑥 ) ) |
5 |
4
|
neeq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ ) ) |
6 |
|
eleq2 |
⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ 𝑓 ↔ 𝑥 ∈ 𝐹 ) ) |
7 |
5 6
|
imbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝑓 ) ↔ ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝑧 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝑓 ) ↔ ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) ) |
9 |
3 8
|
raleqbidv |
⊢ ( ( 𝑧 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑥 ∈ 𝒫 𝑧 ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝑓 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) ) |
10 |
|
fveq2 |
⊢ ( 𝑧 = 𝑋 → ( fBas ‘ 𝑧 ) = ( fBas ‘ 𝑋 ) ) |
11 |
|
fvex |
⊢ ( fBas ‘ 𝑧 ) ∈ V |
12 |
|
elfvdm |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas ) |
13 |
1 9 10 11 12
|
elmptrab2 |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) ) |