Step |
Hyp |
Ref |
Expression |
1 |
|
brdomi |
⊢ ( ω ≼ 𝐴 → ∃ 𝑓 𝑓 : ω –1-1→ 𝐴 ) |
2 |
|
peano1 |
⊢ ∅ ∈ ω |
3 |
|
f1f1orn |
⊢ ( 𝑓 : ω –1-1→ 𝐴 → 𝑓 : ω –1-1-onto→ ran 𝑓 ) |
4 |
3
|
adantr |
⊢ ( ( 𝑓 : ω –1-1→ 𝐴 ∧ 𝐴 = ∅ ) → 𝑓 : ω –1-1-onto→ ran 𝑓 ) |
5 |
|
f1f |
⊢ ( 𝑓 : ω –1-1→ 𝐴 → 𝑓 : ω ⟶ 𝐴 ) |
6 |
5
|
frnd |
⊢ ( 𝑓 : ω –1-1→ 𝐴 → ran 𝑓 ⊆ 𝐴 ) |
7 |
|
sseq0 |
⊢ ( ( ran 𝑓 ⊆ 𝐴 ∧ 𝐴 = ∅ ) → ran 𝑓 = ∅ ) |
8 |
6 7
|
sylan |
⊢ ( ( 𝑓 : ω –1-1→ 𝐴 ∧ 𝐴 = ∅ ) → ran 𝑓 = ∅ ) |
9 |
8
|
f1oeq3d |
⊢ ( ( 𝑓 : ω –1-1→ 𝐴 ∧ 𝐴 = ∅ ) → ( 𝑓 : ω –1-1-onto→ ran 𝑓 ↔ 𝑓 : ω –1-1-onto→ ∅ ) ) |
10 |
4 9
|
mpbid |
⊢ ( ( 𝑓 : ω –1-1→ 𝐴 ∧ 𝐴 = ∅ ) → 𝑓 : ω –1-1-onto→ ∅ ) |
11 |
|
f1ocnv |
⊢ ( 𝑓 : ω –1-1-onto→ ∅ → ◡ 𝑓 : ∅ –1-1-onto→ ω ) |
12 |
|
noel |
⊢ ¬ ∅ ∈ ∅ |
13 |
|
f1o00 |
⊢ ( ◡ 𝑓 : ∅ –1-1-onto→ ω ↔ ( ◡ 𝑓 = ∅ ∧ ω = ∅ ) ) |
14 |
13
|
simprbi |
⊢ ( ◡ 𝑓 : ∅ –1-1-onto→ ω → ω = ∅ ) |
15 |
14
|
eleq2d |
⊢ ( ◡ 𝑓 : ∅ –1-1-onto→ ω → ( ∅ ∈ ω ↔ ∅ ∈ ∅ ) ) |
16 |
12 15
|
mtbiri |
⊢ ( ◡ 𝑓 : ∅ –1-1-onto→ ω → ¬ ∅ ∈ ω ) |
17 |
10 11 16
|
3syl |
⊢ ( ( 𝑓 : ω –1-1→ 𝐴 ∧ 𝐴 = ∅ ) → ¬ ∅ ∈ ω ) |
18 |
2 17
|
mt2 |
⊢ ¬ ( 𝑓 : ω –1-1→ 𝐴 ∧ 𝐴 = ∅ ) |
19 |
18
|
imnani |
⊢ ( 𝑓 : ω –1-1→ 𝐴 → ¬ 𝐴 = ∅ ) |
20 |
19
|
neqned |
⊢ ( 𝑓 : ω –1-1→ 𝐴 → 𝐴 ≠ ∅ ) |
21 |
20
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 : ω –1-1→ 𝐴 → 𝐴 ≠ ∅ ) |
22 |
1 21
|
syl |
⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ ) |