Proof of Theorem rp-isfinite6
Step | Hyp | Ref
| Expression |
1 | | exmid 895 |
. . . 4
⊢ (𝐴 = ∅ ∨ ¬ 𝐴 = ∅) |
2 | 1 | biantrur 534 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ((𝐴 = ∅ ∨ ¬ 𝐴 = ∅) ∧ 𝐴 ∈ Fin)) |
3 | | andir 1009 |
. . 3
⊢ (((𝐴 = ∅ ∨ ¬ 𝐴 = ∅) ∧ 𝐴 ∈ Fin) ↔ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ∨ (¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin))) |
4 | 2, 3 | bitri 278 |
. 2
⊢ (𝐴 ∈ Fin ↔ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ∨ (¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin))) |
5 | | simpl 486 |
. . . 4
⊢ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) → 𝐴 = ∅) |
6 | | 0fin 8854 |
. . . . . 6
⊢ ∅
∈ Fin |
7 | | eleq1a 2833 |
. . . . . 6
⊢ (∅
∈ Fin → (𝐴 =
∅ → 𝐴 ∈
Fin)) |
8 | 6, 7 | ax-mp 5 |
. . . . 5
⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) |
9 | 8 | ancli 552 |
. . . 4
⊢ (𝐴 = ∅ → (𝐴 = ∅ ∧ 𝐴 ∈ Fin)) |
10 | 5, 9 | impbii 212 |
. . 3
⊢ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ↔ 𝐴 = ∅) |
11 | | rp-isfinite5 40817 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0
(1...𝑛) ≈ 𝐴) |
12 | | df-rex 3067 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ0 (1...𝑛)
≈ 𝐴 ↔
∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) |
13 | 11, 12 | bitri 278 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ ∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) |
14 | 13 | anbi2i 626 |
. . . 4
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 ∈ Fin) ↔ (¬ 𝐴 = ∅ ∧ ∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴))) |
15 | | df-rex 3067 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ (1...𝑛) ≈
𝐴 ↔ ∃𝑛(𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) |
16 | | en0 8696 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
17 | | ensymb 8681 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ≈ ∅ ↔ ∅
≈ 𝐴) |
18 | 16, 17 | bitr3i 280 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ ↔ ∅
≈ 𝐴) |
19 | 18 | notbii 323 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 = ∅ ↔ ¬
∅ ≈ 𝐴) |
20 | | elnn0 12097 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℕ
∨ 𝑛 =
0)) |
21 | 20 | anbi1i 627 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴) ↔ ((𝑛 ∈ ℕ ∨ 𝑛 = 0) ∧ (1...𝑛) ≈ 𝐴)) |
22 | | andir 1009 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∨ 𝑛 = 0) ∧ (1...𝑛) ≈ 𝐴) ↔ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) |
23 | 21, 22 | bitri 278 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴) ↔ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) |
24 | 19, 23 | anbi12i 630 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ (¬ ∅ ≈
𝐴 ∧ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) |
25 | | andi 1008 |
. . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
((𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) ↔ ((¬ ∅ ≈ 𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) ∨ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) |
26 | 24, 25 | bitri 278 |
. . . . . . . . . 10
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ ((¬ ∅
≈ 𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) ∨ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) |
27 | | 3anass 1097 |
. . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ↔ (¬ ∅ ≈
𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴))) |
28 | | 3anass 1097 |
. . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴) ↔ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) |
29 | 27, 28 | orbi12i 915 |
. . . . . . . . . 10
⊢ (((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ∨ (¬ ∅ ≈
𝐴 ∧ 𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)) ↔ ((¬ ∅ ≈ 𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) ∨ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) |
30 | 26, 29 | sylbb2 241 |
. . . . . . . . 9
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → ((¬ ∅
≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) |
31 | | simp2 1139 |
. . . . . . . . . 10
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) → 𝑛 ∈ ℕ) |
32 | | oveq2 7226 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (1...𝑛) = (1...0)) |
33 | | fz10 13138 |
. . . . . . . . . . . 12
⊢ (1...0) =
∅ |
34 | 32, 33 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → (1...𝑛) = ∅) |
35 | | simp2 1139 |
. . . . . . . . . . . . 13
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → (1...𝑛) = ∅) |
36 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → (1...𝑛) ≈ 𝐴) |
37 | 35, 36 | eqbrtrrd 5082 |
. . . . . . . . . . . 12
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → ∅ ≈ 𝐴) |
38 | | simp1 1138 |
. . . . . . . . . . . 12
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → ¬ ∅ ≈
𝐴) |
39 | 37, 38 | pm2.21dd 198 |
. . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → 𝑛 ∈ ℕ) |
40 | 34, 39 | syl3an2 1166 |
. . . . . . . . . 10
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴) → 𝑛 ∈ ℕ) |
41 | 31, 40 | jaoi 857 |
. . . . . . . . 9
⊢ (((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ∨ (¬ ∅ ≈
𝐴 ∧ 𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)) → 𝑛 ∈ ℕ) |
42 | 30, 41 | syl 17 |
. . . . . . . 8
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → 𝑛 ∈ ℕ) |
43 | | simprr 773 |
. . . . . . . 8
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → (1...𝑛) ≈ 𝐴) |
44 | 42, 43 | jca 515 |
. . . . . . 7
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) |
45 | | nngt0 11866 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) |
46 | | hash0 13939 |
. . . . . . . . . . . . 13
⊢
(♯‘∅) = 0 |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(♯‘∅) = 0) |
48 | | nnnn0 12102 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
49 | | hashfz1 13917 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (♯‘(1...𝑛)) = 𝑛) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(♯‘(1...𝑛)) =
𝑛) |
51 | 45, 47, 50 | 3brtr4d 5090 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(♯‘∅) < (♯‘(1...𝑛))) |
52 | | fzfi 13550 |
. . . . . . . . . . . 12
⊢
(1...𝑛) ∈
Fin |
53 | | hashsdom 13953 |
. . . . . . . . . . . 12
⊢ ((∅
∈ Fin ∧ (1...𝑛)
∈ Fin) → ((♯‘∅) < (♯‘(1...𝑛)) ↔ ∅ ≺
(1...𝑛))) |
54 | 6, 52, 53 | mp2an 692 |
. . . . . . . . . . 11
⊢
((♯‘∅) < (♯‘(1...𝑛)) ↔ ∅ ≺ (1...𝑛)) |
55 | 51, 54 | sylib 221 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ∅
≺ (1...𝑛)) |
56 | 55 | anim1i 618 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → (∅ ≺ (1...𝑛) ∧ (1...𝑛) ≈ 𝐴)) |
57 | | sdomentr 8785 |
. . . . . . . . . . 11
⊢ ((∅
≺ (1...𝑛) ∧
(1...𝑛) ≈ 𝐴) → ∅ ≺ 𝐴) |
58 | | sdomnen 8662 |
. . . . . . . . . . 11
⊢ (∅
≺ 𝐴 → ¬
∅ ≈ 𝐴) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((∅
≺ (1...𝑛) ∧
(1...𝑛) ≈ 𝐴) → ¬ ∅ ≈
𝐴) |
60 | | ensymb 8681 |
. . . . . . . . . . . 12
⊢ (∅
≈ 𝐴 ↔ 𝐴 ≈
∅) |
61 | 60, 16 | bitri 278 |
. . . . . . . . . . 11
⊢ (∅
≈ 𝐴 ↔ 𝐴 = ∅) |
62 | 61 | notbii 323 |
. . . . . . . . . 10
⊢ (¬
∅ ≈ 𝐴 ↔
¬ 𝐴 =
∅) |
63 | 59, 62 | sylib 221 |
. . . . . . . . 9
⊢ ((∅
≺ (1...𝑛) ∧
(1...𝑛) ≈ 𝐴) → ¬ 𝐴 = ∅) |
64 | 56, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → ¬ 𝐴 = ∅) |
65 | 48 | anim1i 618 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → (𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) |
66 | 64, 65 | jca 515 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → (¬ 𝐴 = ∅ ∧ (𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴))) |
67 | 44, 66 | impbii 212 |
. . . . . 6
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) |
68 | 67 | exbii 1855 |
. . . . 5
⊢
(∃𝑛(¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ ∃𝑛(𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) |
69 | | 19.42v 1962 |
. . . . 5
⊢
(∃𝑛(¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ (¬ 𝐴 = ∅ ∧ ∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴))) |
70 | 15, 68, 69 | 3bitr2ri 303 |
. . . 4
⊢ ((¬
𝐴 = ∅ ∧
∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) ↔ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴) |
71 | 14, 70 | bitri 278 |
. . 3
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 ∈ Fin) ↔ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴) |
72 | 10, 71 | orbi12i 915 |
. 2
⊢ (((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ∨ (¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin)) ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴)) |
73 | 4, 72 | bitri 278 |
1
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴)) |