Step | Hyp | Ref
| Expression |
1 | | ennnfone 12367 |
. . . 4
⊢ (𝐴 ≈ ℕ ↔
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑔(𝑔:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖)))) |
2 | 1 | simplbi 272 |
. . 3
⊢ (𝐴 ≈ ℕ →
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
3 | | nnenom 10377 |
. . . . . . 7
⊢ ℕ
≈ ω |
4 | | entr 6758 |
. . . . . . 7
⊢ ((𝐴 ≈ ℕ ∧ ℕ
≈ ω) → 𝐴
≈ ω) |
5 | 3, 4 | mpan2 423 |
. . . . . 6
⊢ (𝐴 ≈ ℕ → 𝐴 ≈
ω) |
6 | 5 | ensymd 6757 |
. . . . 5
⊢ (𝐴 ≈ ℕ → ω
≈ 𝐴) |
7 | | bren 6721 |
. . . . 5
⊢ (ω
≈ 𝐴 ↔
∃𝑓 𝑓:ω–1-1-onto→𝐴) |
8 | 6, 7 | sylib 121 |
. . . 4
⊢ (𝐴 ≈ ℕ →
∃𝑓 𝑓:ω–1-1-onto→𝐴) |
9 | | f1ofo 5447 |
. . . . . . . 8
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴) |
10 | 9 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑓:ω–onto→𝐴) |
11 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω) |
12 | | nnord 4594 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → Ord 𝑛) |
13 | 12 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → Ord 𝑛) |
14 | | ordirr 4524 |
. . . . . . . . . . 11
⊢ (Ord
𝑛 → ¬ 𝑛 ∈ 𝑛) |
15 | 13, 14 | syl 14 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → ¬ 𝑛 ∈ 𝑛) |
16 | | f1of1 5439 |
. . . . . . . . . . . 12
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–1-1→𝐴) |
17 | 16 | ad2antlr 486 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → 𝑓:ω–1-1→𝐴) |
18 | | omelon 4591 |
. . . . . . . . . . . . 13
⊢ ω
∈ On |
19 | 18 | onelssi 4412 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → 𝑛 ⊆
ω) |
20 | 19 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ⊆ ω) |
21 | | f1elima 5749 |
. . . . . . . . . . 11
⊢ ((𝑓:ω–1-1→𝐴 ∧ 𝑛 ∈ ω ∧ 𝑛 ⊆ ω) → ((𝑓‘𝑛) ∈ (𝑓 “ 𝑛) ↔ 𝑛 ∈ 𝑛)) |
22 | 17, 11, 20, 21 | syl3anc 1233 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → ((𝑓‘𝑛) ∈ (𝑓 “ 𝑛) ↔ 𝑛 ∈ 𝑛)) |
23 | 15, 22 | mtbird 668 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → ¬ (𝑓‘𝑛) ∈ (𝑓 “ 𝑛)) |
24 | | fveq2 5494 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑓‘𝑘) = (𝑓‘𝑛)) |
25 | 24 | eleq1d 2239 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → ((𝑓‘𝑘) ∈ (𝑓 “ 𝑛) ↔ (𝑓‘𝑛) ∈ (𝑓 “ 𝑛))) |
26 | 25 | notbid 662 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛) ↔ ¬ (𝑓‘𝑛) ∈ (𝑓 “ 𝑛))) |
27 | 26 | rspcev 2834 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ω ∧ ¬
(𝑓‘𝑛) ∈ (𝑓 “ 𝑛)) → ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) |
28 | 11, 23, 27 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) ∧ 𝑛 ∈ ω) → ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) |
29 | 28 | ralrimiva 2543 |
. . . . . . 7
⊢ ((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) |
30 | 10, 29 | jca 304 |
. . . . . 6
⊢ ((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto→𝐴) → (𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛))) |
31 | 30 | ex 114 |
. . . . 5
⊢ (𝐴 ≈ ℕ → (𝑓:ω–1-1-onto→𝐴 → (𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)))) |
32 | 31 | eximdv 1873 |
. . . 4
⊢ (𝐴 ≈ ℕ →
(∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)))) |
33 | 8, 32 | mpd 13 |
. . 3
⊢ (𝐴 ≈ ℕ →
∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛))) |
34 | 2, 33 | jca 304 |
. 2
⊢ (𝐴 ≈ ℕ →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)))) |
35 | | oveq1 5857 |
. . . . . . . . 9
⊢ (𝑏 = 𝑎 → (𝑏 + 1) = (𝑎 + 1)) |
36 | 35 | cbvmptv 4083 |
. . . . . . . 8
⊢ (𝑏 ∈ ℤ ↦ (𝑏 + 1)) = (𝑎 ∈ ℤ ↦ (𝑎 + 1)) |
37 | | freceq1 6368 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ↦ (𝑏 + 1)) = (𝑎 ∈ ℤ ↦ (𝑎 + 1)) → frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0) = frec((𝑎 ∈ ℤ ↦ (𝑎 + 1)), 0)) |
38 | 36, 37 | ax-mp 5 |
. . . . . . 7
⊢
frec((𝑏 ∈
ℤ ↦ (𝑏 + 1)),
0) = frec((𝑎 ∈ ℤ
↦ (𝑎 + 1)),
0) |
39 | | eqid 2170 |
. . . . . . 7
⊢ (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) |
40 | | simpl 108 |
. . . . . . 7
⊢ ((𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) → 𝑓:ω–onto→𝐴) |
41 | | fveq2 5494 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑑 → (𝑓‘𝑘) = (𝑓‘𝑑)) |
42 | 41 | eleq1d 2239 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑑 → ((𝑓‘𝑘) ∈ (𝑓 “ 𝑛) ↔ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛))) |
43 | 42 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑑 → (¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛) ↔ ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛))) |
44 | 43 | cbvrexv 2697 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛) ↔ ∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛)) |
45 | 44 | ralbii 2476 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω ∃𝑘 ∈
ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛) ↔ ∀𝑛 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛)) |
46 | | imaeq2 4947 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑐 → (𝑓 “ 𝑛) = (𝑓 “ 𝑐)) |
47 | 46 | eleq2d 2240 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑐 → ((𝑓‘𝑑) ∈ (𝑓 “ 𝑛) ↔ (𝑓‘𝑑) ∈ (𝑓 “ 𝑐))) |
48 | 47 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑐 → (¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛) ↔ ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑐))) |
49 | 48 | rexbidv 2471 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑐 → (∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛) ↔ ∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑐))) |
50 | 49 | cbvralv 2696 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω ∃𝑑 ∈
ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑛) ↔ ∀𝑐 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑐)) |
51 | 45, 50 | sylbb 122 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω ∃𝑘 ∈
ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛) → ∀𝑐 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑐)) |
52 | 51 | adantl 275 |
. . . . . . 7
⊢ ((𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) → ∀𝑐 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓‘𝑑) ∈ (𝑓 “ 𝑐)) |
53 | 38, 39, 40, 52 | ctinfomlemom 12369 |
. . . . . 6
⊢ ((𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) → ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))) |
54 | | vex 2733 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
55 | | frecex 6370 |
. . . . . . . . 9
⊢
frec((𝑏 ∈
ℤ ↦ (𝑏 + 1)),
0) ∈ V |
56 | 55 | cnvex 5147 |
. . . . . . . 8
⊢ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0) ∈ V |
57 | 54, 56 | coex 5154 |
. . . . . . 7
⊢ (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) ∈ V |
58 | | foeq1 5414 |
. . . . . . . 8
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (𝑔:ℕ0–onto→𝐴 ↔ (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0–onto→𝐴)) |
59 | | fveq1 5493 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (𝑔‘𝑗) = ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗)) |
60 | | fveq1 5493 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (𝑔‘𝑖) = ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)) |
61 | 59, 60 | neeq12d 2360 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → ((𝑔‘𝑗) ≠ (𝑔‘𝑖) ↔ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))) |
62 | 61 | ralbidv 2470 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖) ↔ ∀𝑖 ∈ (0...𝑚)((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))) |
63 | 62 | rexbidv 2471 |
. . . . . . . . 9
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (∃𝑗 ∈ ℕ0 ∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖) ↔ ∃𝑗 ∈ ℕ0 ∀𝑖 ∈ (0...𝑚)((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))) |
64 | 63 | ralbidv 2470 |
. . . . . . . 8
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (∀𝑚 ∈ ℕ0
∃𝑗 ∈
ℕ0 ∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖) ↔ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))) |
65 | 58, 64 | anbi12d 470 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → ((𝑔:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖)) ↔ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)))) |
66 | 57, 65 | spcev 2825 |
. . . . . 6
⊢ (((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓 ∘ ◡frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)) → ∃𝑔(𝑔:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖))) |
67 | 53, 66 | syl 14 |
. . . . 5
⊢ ((𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) → ∃𝑔(𝑔:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖))) |
68 | 67 | exlimiv 1591 |
. . . 4
⊢
(∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)) → ∃𝑔(𝑔:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖))) |
69 | 68 | anim2i 340 |
. . 3
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛))) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑔(𝑔:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈ (0...𝑚)(𝑔‘𝑗) ≠ (𝑔‘𝑖)))) |
70 | 69, 1 | sylibr 133 |
. 2
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛))) → 𝐴 ≈ ℕ) |
71 | 34, 70 | impbii 125 |
1
⊢ (𝐴 ≈ ℕ ↔
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)))) |