Step |
Hyp |
Ref |
Expression |
1 |
|
peano1 |
⊢ ∅ ∈ ω |
2 |
|
peano2 |
⊢ ( ∅ ∈ ω → suc ∅ ∈ ω ) |
3 |
1 2
|
ax-mp |
⊢ suc ∅ ∈ ω |
4 |
|
0elpw |
⊢ ∅ ∈ 𝒫 ( 𝑅1 ‘ ∅ ) |
5 |
|
0elon |
⊢ ∅ ∈ On |
6 |
|
r1suc |
⊢ ( ∅ ∈ On → ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ ) ) |
7 |
5 6
|
ax-mp |
⊢ ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ ) |
8 |
4 7
|
eleqtrri |
⊢ ∅ ∈ ( 𝑅1 ‘ suc ∅ ) |
9 |
|
fveq2 |
⊢ ( 𝑥 = suc ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc ∅ ) ) |
10 |
9
|
eleq2d |
⊢ ( 𝑥 = suc ∅ → ( ∅ ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∅ ∈ ( 𝑅1 ‘ suc ∅ ) ) ) |
11 |
10
|
rspcev |
⊢ ( ( suc ∅ ∈ ω ∧ ∅ ∈ ( 𝑅1 ‘ suc ∅ ) ) → ∃ 𝑥 ∈ ω ∅ ∈ ( 𝑅1 ‘ 𝑥 ) ) |
12 |
3 8 11
|
mp2an |
⊢ ∃ 𝑥 ∈ ω ∅ ∈ ( 𝑅1 ‘ 𝑥 ) |
13 |
|
elhf |
⊢ ( ∅ ∈ Hf ↔ ∃ 𝑥 ∈ ω ∅ ∈ ( 𝑅1 ‘ 𝑥 ) ) |
14 |
12 13
|
mpbir |
⊢ ∅ ∈ Hf |