Step |
Hyp |
Ref |
Expression |
1 |
|
df-fg |
⊢ filGen = ( 𝑣 ∈ V , 𝑓 ∈ ( fBas ‘ 𝑣 ) ↦ { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } ) |
2 |
1
|
a1i |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → filGen = ( 𝑣 ∈ V , 𝑓 ∈ ( fBas ‘ 𝑣 ) ↦ { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } ) ) |
3 |
|
pweq |
⊢ ( 𝑣 = 𝑋 → 𝒫 𝑣 = 𝒫 𝑋 ) |
4 |
3
|
adantr |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑓 = 𝐹 ) → 𝒫 𝑣 = 𝒫 𝑋 ) |
5 |
|
ineq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∩ 𝒫 𝑥 ) = ( 𝐹 ∩ 𝒫 𝑥 ) ) |
6 |
5
|
neeq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ ) ) |
7 |
6
|
adantl |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ ) ) |
8 |
4 7
|
rabeqbidv |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑓 = 𝐹 ) → { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ) |
9 |
8
|
adantl |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑣 = 𝑋 ∧ 𝑓 = 𝐹 ) ) → { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ) |
10 |
|
fveq2 |
⊢ ( 𝑣 = 𝑋 → ( fBas ‘ 𝑣 ) = ( fBas ‘ 𝑋 ) ) |
11 |
10
|
adantl |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑣 = 𝑋 ) → ( fBas ‘ 𝑣 ) = ( fBas ‘ 𝑋 ) ) |
12 |
|
elfvex |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ V ) |
13 |
|
id |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) ) |
14 |
|
elfvdm |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas ) |
15 |
|
pwexg |
⊢ ( 𝑋 ∈ dom fBas → 𝒫 𝑋 ∈ V ) |
16 |
|
rabexg |
⊢ ( 𝒫 𝑋 ∈ V → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ∈ V ) |
17 |
14 15 16
|
3syl |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ∈ V ) |
18 |
2 9 11 12 13 17
|
ovmpodx |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ) |