Proof of Theorem rp-isfinite6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | exmid 895 | . . . 4
⊢ (𝐴 = ∅ ∨ ¬ 𝐴 = ∅) | 
| 2 | 1 | biantrur 530 | . . 3
⊢ (𝐴 ∈ Fin ↔ ((𝐴 = ∅ ∨ ¬ 𝐴 = ∅) ∧ 𝐴 ∈ Fin)) | 
| 3 |  | andir 1011 | . . 3
⊢ (((𝐴 = ∅ ∨ ¬ 𝐴 = ∅) ∧ 𝐴 ∈ Fin) ↔ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ∨ (¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin))) | 
| 4 | 2, 3 | bitri 275 | . 2
⊢ (𝐴 ∈ Fin ↔ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ∨ (¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin))) | 
| 5 |  | simpl 482 | . . . 4
⊢ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) → 𝐴 = ∅) | 
| 6 |  | 0fi 9082 | . . . . . 6
⊢ ∅
∈ Fin | 
| 7 |  | eleq1a 2836 | . . . . . 6
⊢ (∅
∈ Fin → (𝐴 =
∅ → 𝐴 ∈
Fin)) | 
| 8 | 6, 7 | ax-mp 5 | . . . . 5
⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) | 
| 9 | 8 | ancli 548 | . . . 4
⊢ (𝐴 = ∅ → (𝐴 = ∅ ∧ 𝐴 ∈ Fin)) | 
| 10 | 5, 9 | impbii 209 | . . 3
⊢ ((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ↔ 𝐴 = ∅) | 
| 11 |  | rp-isfinite5 43530 | . . . . . 6
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0
(1...𝑛) ≈ 𝐴) | 
| 12 |  | df-rex 3071 | . . . . . 6
⊢
(∃𝑛 ∈
ℕ0 (1...𝑛)
≈ 𝐴 ↔
∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) | 
| 13 | 11, 12 | bitri 275 | . . . . 5
⊢ (𝐴 ∈ Fin ↔ ∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) | 
| 14 | 13 | anbi2i 623 | . . . 4
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 ∈ Fin) ↔ (¬ 𝐴 = ∅ ∧ ∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 15 |  | df-rex 3071 | . . . . 5
⊢
(∃𝑛 ∈
ℕ (1...𝑛) ≈
𝐴 ↔ ∃𝑛(𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) | 
| 16 |  | en0 9058 | . . . . . . . . . . . . . 14
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | 
| 17 |  | ensymb 9042 | . . . . . . . . . . . . . 14
⊢ (𝐴 ≈ ∅ ↔ ∅
≈ 𝐴) | 
| 18 | 16, 17 | bitr3i 277 | . . . . . . . . . . . . 13
⊢ (𝐴 = ∅ ↔ ∅
≈ 𝐴) | 
| 19 | 18 | notbii 320 | . . . . . . . . . . . 12
⊢ (¬
𝐴 = ∅ ↔ ¬
∅ ≈ 𝐴) | 
| 20 |  | elnn0 12528 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℕ
∨ 𝑛 =
0)) | 
| 21 | 20 | anbi1i 624 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴) ↔ ((𝑛 ∈ ℕ ∨ 𝑛 = 0) ∧ (1...𝑛) ≈ 𝐴)) | 
| 22 |  | andir 1011 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∨ 𝑛 = 0) ∧ (1...𝑛) ≈ 𝐴) ↔ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 23 | 21, 22 | bitri 275 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴) ↔ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 24 | 19, 23 | anbi12i 628 | . . . . . . . . . . 11
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ (¬ ∅ ≈
𝐴 ∧ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) | 
| 25 |  | andi 1010 | . . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
((𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ∨ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) ↔ ((¬ ∅ ≈ 𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) ∨ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) | 
| 26 | 24, 25 | bitri 275 | . . . . . . . . . 10
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ ((¬ ∅
≈ 𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) ∨ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) | 
| 27 |  | 3anass 1095 | . . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ↔ (¬ ∅ ≈
𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴))) | 
| 28 |  | 3anass 1095 | . . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴) ↔ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 29 | 27, 28 | orbi12i 915 | . . . . . . . . . 10
⊢ (((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ∨ (¬ ∅ ≈
𝐴 ∧ 𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)) ↔ ((¬ ∅ ≈ 𝐴 ∧ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) ∨ (¬ ∅ ≈ 𝐴 ∧ (𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)))) | 
| 30 | 26, 29 | sylbb2 238 | . . . . . . . . 9
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → ((¬ ∅
≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) ∨ (¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 31 |  | simp2 1138 | . . . . . . . . . 10
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) → 𝑛 ∈ ℕ) | 
| 32 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑛 = 0 → (1...𝑛) = (1...0)) | 
| 33 |  | fz10 13585 | . . . . . . . . . . . 12
⊢ (1...0) =
∅ | 
| 34 | 32, 33 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (𝑛 = 0 → (1...𝑛) = ∅) | 
| 35 |  | simp2 1138 | . . . . . . . . . . . . 13
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → (1...𝑛) = ∅) | 
| 36 |  | simp3 1139 | . . . . . . . . . . . . 13
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → (1...𝑛) ≈ 𝐴) | 
| 37 | 35, 36 | eqbrtrrd 5167 | . . . . . . . . . . . 12
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → ∅ ≈ 𝐴) | 
| 38 |  | simp1 1137 | . . . . . . . . . . . 12
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → ¬ ∅ ≈
𝐴) | 
| 39 | 37, 38 | pm2.21dd 195 | . . . . . . . . . . 11
⊢ ((¬
∅ ≈ 𝐴 ∧
(1...𝑛) = ∅ ∧
(1...𝑛) ≈ 𝐴) → 𝑛 ∈ ℕ) | 
| 40 | 34, 39 | syl3an2 1165 | . . . . . . . . . 10
⊢ ((¬
∅ ≈ 𝐴 ∧
𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴) → 𝑛 ∈ ℕ) | 
| 41 | 31, 40 | jaoi 858 | . . . . . . . . 9
⊢ (((¬
∅ ≈ 𝐴 ∧
𝑛 ∈ ℕ ∧
(1...𝑛) ≈ 𝐴) ∨ (¬ ∅ ≈
𝐴 ∧ 𝑛 = 0 ∧ (1...𝑛) ≈ 𝐴)) → 𝑛 ∈ ℕ) | 
| 42 | 30, 41 | syl 17 | . . . . . . . 8
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → 𝑛 ∈ ℕ) | 
| 43 |  | simprr 773 | . . . . . . . 8
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → (1...𝑛) ≈ 𝐴) | 
| 44 | 42, 43 | jca 511 | . . . . . . 7
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) → (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) | 
| 45 |  | nngt0 12297 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) | 
| 46 |  | hash0 14406 | . . . . . . . . . . . . 13
⊢
(♯‘∅) = 0 | 
| 47 | 46 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(♯‘∅) = 0) | 
| 48 |  | nnnn0 12533 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 49 |  | hashfz1 14385 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (♯‘(1...𝑛)) = 𝑛) | 
| 50 | 48, 49 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(♯‘(1...𝑛)) =
𝑛) | 
| 51 | 45, 47, 50 | 3brtr4d 5175 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(♯‘∅) < (♯‘(1...𝑛))) | 
| 52 |  | fzfi 14013 | . . . . . . . . . . . 12
⊢
(1...𝑛) ∈
Fin | 
| 53 |  | hashsdom 14420 | . . . . . . . . . . . 12
⊢ ((∅
∈ Fin ∧ (1...𝑛)
∈ Fin) → ((♯‘∅) < (♯‘(1...𝑛)) ↔ ∅ ≺
(1...𝑛))) | 
| 54 | 6, 52, 53 | mp2an 692 | . . . . . . . . . . 11
⊢
((♯‘∅) < (♯‘(1...𝑛)) ↔ ∅ ≺ (1...𝑛)) | 
| 55 | 51, 54 | sylib 218 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ∅
≺ (1...𝑛)) | 
| 56 | 55 | anim1i 615 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → (∅ ≺ (1...𝑛) ∧ (1...𝑛) ≈ 𝐴)) | 
| 57 |  | sdomentr 9151 | . . . . . . . . . . 11
⊢ ((∅
≺ (1...𝑛) ∧
(1...𝑛) ≈ 𝐴) → ∅ ≺ 𝐴) | 
| 58 |  | sdomnen 9021 | . . . . . . . . . . 11
⊢ (∅
≺ 𝐴 → ¬
∅ ≈ 𝐴) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . 10
⊢ ((∅
≺ (1...𝑛) ∧
(1...𝑛) ≈ 𝐴) → ¬ ∅ ≈
𝐴) | 
| 60 |  | en0r 9060 | . . . . . . . . . . 11
⊢ (∅
≈ 𝐴 ↔ 𝐴 = ∅) | 
| 61 | 60 | notbii 320 | . . . . . . . . . 10
⊢ (¬
∅ ≈ 𝐴 ↔
¬ 𝐴 =
∅) | 
| 62 | 59, 61 | sylib 218 | . . . . . . . . 9
⊢ ((∅
≺ (1...𝑛) ∧
(1...𝑛) ≈ 𝐴) → ¬ 𝐴 = ∅) | 
| 63 | 56, 62 | syl 17 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → ¬ 𝐴 = ∅) | 
| 64 | 48 | anim1i 615 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → (𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) | 
| 65 | 63, 64 | jca 511 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴) → (¬ 𝐴 = ∅ ∧ (𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 66 | 44, 65 | impbii 209 | . . . . . 6
⊢ ((¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ (𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) | 
| 67 | 66 | exbii 1848 | . . . . 5
⊢
(∃𝑛(¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ ∃𝑛(𝑛 ∈ ℕ ∧ (1...𝑛) ≈ 𝐴)) | 
| 68 |  | 19.42v 1953 | . . . . 5
⊢
(∃𝑛(¬
𝐴 = ∅ ∧ (𝑛 ∈ ℕ0
∧ (1...𝑛) ≈ 𝐴)) ↔ (¬ 𝐴 = ∅ ∧ ∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴))) | 
| 69 | 15, 67, 68 | 3bitr2ri 300 | . . . 4
⊢ ((¬
𝐴 = ∅ ∧
∃𝑛(𝑛 ∈ ℕ0 ∧ (1...𝑛) ≈ 𝐴)) ↔ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴) | 
| 70 | 14, 69 | bitri 275 | . . 3
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 ∈ Fin) ↔ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴) | 
| 71 | 10, 70 | orbi12i 915 | . 2
⊢ (((𝐴 = ∅ ∧ 𝐴 ∈ Fin) ∨ (¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin)) ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴)) | 
| 72 | 4, 71 | bitri 275 | 1
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴)) |