Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
|
fival |
⊢ ( ∅ ∈ V → ( fi ‘ ∅ ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 } ) |
3 |
1 2
|
ax-mp |
⊢ ( fi ‘ ∅ ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 } |
4 |
|
vprc |
⊢ ¬ V ∈ V |
5 |
|
id |
⊢ ( 𝑦 = ∩ 𝑥 → 𝑦 = ∩ 𝑥 ) |
6 |
|
elinel1 |
⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 ∈ 𝒫 ∅ ) |
7 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 ∅ → 𝑥 ⊆ ∅ ) |
8 |
|
ss0 |
⊢ ( 𝑥 ⊆ ∅ → 𝑥 = ∅ ) |
9 |
6 7 8
|
3syl |
⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 = ∅ ) |
10 |
9
|
inteqd |
⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → ∩ 𝑥 = ∩ ∅ ) |
11 |
|
int0 |
⊢ ∩ ∅ = V |
12 |
10 11
|
eqtrdi |
⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → ∩ 𝑥 = V ) |
13 |
5 12
|
sylan9eqr |
⊢ ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 = V ) |
14 |
13
|
rexlimiva |
⊢ ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 → 𝑦 = V ) |
15 |
|
vex |
⊢ 𝑦 ∈ V |
16 |
14 15
|
eqeltrrdi |
⊢ ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 → V ∈ V ) |
17 |
4 16
|
mto |
⊢ ¬ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 |
18 |
17
|
abf |
⊢ { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 } = ∅ |
19 |
3 18
|
eqtri |
⊢ ( fi ‘ ∅ ) = ∅ |