Step |
Hyp |
Ref |
Expression |
0 |
|
cufil |
⊢ UFil |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
vf |
⊢ 𝑓 |
4 |
|
cfil |
⊢ Fil |
5 |
1
|
cv |
⊢ 𝑔 |
6 |
5 4
|
cfv |
⊢ ( Fil ‘ 𝑔 ) |
7 |
|
vx |
⊢ 𝑥 |
8 |
5
|
cpw |
⊢ 𝒫 𝑔 |
9 |
7
|
cv |
⊢ 𝑥 |
10 |
3
|
cv |
⊢ 𝑓 |
11 |
9 10
|
wcel |
⊢ 𝑥 ∈ 𝑓 |
12 |
5 9
|
cdif |
⊢ ( 𝑔 ∖ 𝑥 ) |
13 |
12 10
|
wcel |
⊢ ( 𝑔 ∖ 𝑥 ) ∈ 𝑓 |
14 |
11 13
|
wo |
⊢ ( 𝑥 ∈ 𝑓 ∨ ( 𝑔 ∖ 𝑥 ) ∈ 𝑓 ) |
15 |
14 7 8
|
wral |
⊢ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥 ∈ 𝑓 ∨ ( 𝑔 ∖ 𝑥 ) ∈ 𝑓 ) |
16 |
15 3 6
|
crab |
⊢ { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥 ∈ 𝑓 ∨ ( 𝑔 ∖ 𝑥 ) ∈ 𝑓 ) } |
17 |
1 2 16
|
cmpt |
⊢ ( 𝑔 ∈ V ↦ { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥 ∈ 𝑓 ∨ ( 𝑔 ∖ 𝑥 ) ∈ 𝑓 ) } ) |
18 |
0 17
|
wceq |
⊢ UFil = ( 𝑔 ∈ V ↦ { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥 ∈ 𝑓 ∨ ( 𝑔 ∖ 𝑥 ) ∈ 𝑓 ) } ) |