Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ ) |
2 |
|
reldom |
⊢ Rel ≼ |
3 |
2
|
a1i |
⊢ ( 𝐴 ≼ ω → Rel ≼ ) |
4 |
|
brrelex1 |
⊢ ( ( Rel ≼ ∧ 𝐴 ≼ ω ) → 𝐴 ∈ V ) |
5 |
3 4
|
mpancom |
⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V ) |
6 |
|
0sdomg |
⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
7 |
5 6
|
syl |
⊢ ( 𝐴 ≼ ω → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
9 |
1 8
|
mpbird |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∅ ≺ 𝐴 ) |
10 |
|
nnenom |
⊢ ℕ ≈ ω |
11 |
10
|
ensymi |
⊢ ω ≈ ℕ |
12 |
11
|
a1i |
⊢ ( 𝐴 ≼ ω → ω ≈ ℕ ) |
13 |
|
domentr |
⊢ ( ( 𝐴 ≼ ω ∧ ω ≈ ℕ ) → 𝐴 ≼ ℕ ) |
14 |
12 13
|
mpdan |
⊢ ( 𝐴 ≼ ω → 𝐴 ≼ ℕ ) |
15 |
14
|
adantr |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → 𝐴 ≼ ℕ ) |
16 |
|
fodomr |
⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 ) |
17 |
9 15 16
|
syl2anc |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 ) |