Metamath Proof Explorer

Theorem rp-isfinite6

Description: A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN . (Contributed by RP, 10-Mar-2020)

Ref Expression
Assertion rp-isfinite6 ( 𝐴 ∈ Fin ↔ ( 𝐴 = ∅ ∨ ∃ 𝑛 ∈ ℕ ( 1 ... 𝑛 ) ≈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 exmid ⊢ ( 𝐴 = ∅ ∨ ¬ 𝐴 = ∅ )
2 1 biantrur ⊢ ( 𝐴 ∈ Fin ↔ ( ( 𝐴 = ∅ ∨ ¬ 𝐴 = ∅ ) ∧ 𝐴 ∈ Fin ) )
3 andir ⊢ ( ( ( 𝐴 = ∅ ∨ ¬ 𝐴 = ∅ ) ∧ 𝐴 ∈ Fin ) ↔ ( ( 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ∨ ( ¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ) )
4 2 3 bitri ⊢ ( 𝐴 ∈ Fin ↔ ( ( 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ∨ ( ¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ) )
5 simpl ⊢ ( ( 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 = ∅ )
6 0fi ⊢ ∅ ∈ Fin
7 eleq1a ⊢ ( ∅ ∈ Fin → ( 𝐴 = ∅ → 𝐴 ∈ Fin ) )
8 6 7 ax-mp ⊢ ( 𝐴 = ∅ → 𝐴 ∈ Fin )
9 8 ancli ⊢ ( 𝐴 = ∅ → ( 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) )
10 5 9 impbii ⊢ ( ( 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ↔ 𝐴 = ∅ )
11 rp-isfinite5 ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 )
12 df-rex ⊢ ( ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
13 11 12 bitri ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
14 13 anbi2i ⊢ ( ( ¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ↔ ( ¬ 𝐴 = ∅ ∧ ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
15 df-rex ⊢ ( ∃ 𝑛 ∈ ℕ ( 1 ... 𝑛 ) ≈ 𝐴 ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
16 en0 ⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
17 ensymb ⊢ ( 𝐴 ≈ ∅ ↔ ∅ ≈ 𝐴 )
18 16 17 bitr3i ⊢ ( 𝐴 = ∅ ↔ ∅ ≈ 𝐴 )
19 18 notbii ⊢ ( ¬ 𝐴 = ∅ ↔ ¬ ∅ ≈ 𝐴 )
20 elnn0 ⊢ ( 𝑛 ∈ ℕ0 ↔ ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) )
21 20 anbi1i ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ↔ ( ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
22 andir ⊢ ( ( ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
23 21 22 bitri ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
24 19 23 anbi12i ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ( ¬ ∅ ≈ 𝐴 ∧ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ) )
25 andi ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ) ↔ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ∨ ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ) )
26 24 25 bitri ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ∨ ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ) )
27 3anass ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ↔ ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
28 3anass ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ↔ ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
29 27 28 orbi12i ⊢ ( ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ∨ ( ¬ ∅ ≈ 𝐴 ∧ ( 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ) )
30 26 29 sylbb2 ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) → ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
31 simp2 ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → 𝑛 ∈ ℕ )
32 oveq2 ⊢ ( 𝑛 = 0 → ( 1 ... 𝑛 ) = ( 1 ... 0 ) )
33 fz10 ⊢ ( 1 ... 0 ) = ∅
34 32 33 eqtrdi ⊢ ( 𝑛 = 0 → ( 1 ... 𝑛 ) = ∅ )
35 simp2 ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 1 ... 𝑛 ) = ∅ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( 1 ... 𝑛 ) = ∅ )
36 simp3 ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 1 ... 𝑛 ) = ∅ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( 1 ... 𝑛 ) ≈ 𝐴 )
37 35 36 eqbrtrrd ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 1 ... 𝑛 ) = ∅ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ∅ ≈ 𝐴 )
38 simp1 ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 1 ... 𝑛 ) = ∅ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ¬ ∅ ≈ 𝐴 )
39 37 38 pm2.21dd ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ ( 1 ... 𝑛 ) = ∅ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → 𝑛 ∈ ℕ )
40 34 39 syl3an2 ⊢ ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → 𝑛 ∈ ℕ )
41 31 40 jaoi ⊢ ( ( ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ∨ ( ¬ ∅ ≈ 𝐴 ∧ 𝑛 = 0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) → 𝑛 ∈ ℕ )
42 30 41 syl ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) → 𝑛 ∈ ℕ )
43 simprr ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) → ( 1 ... 𝑛 ) ≈ 𝐴 )
44 42 43 jca ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) → ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
45 nngt0 ⊢ ( 𝑛 ∈ ℕ → 0 < 𝑛 )
46 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
47 46 a1i ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ∅ ) = 0 )
48 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
49 hashfz1 ⊢ ( 𝑛 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
50 48 49 syl ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
51 45 47 50 3brtr4d ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ∅ ) < ( ♯ ‘ ( 1 ... 𝑛 ) ) )
52 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
53 hashsdom ⊢ ( ( ∅ ∈ Fin ∧ ( 1 ... 𝑛 ) ∈ Fin ) → ( ( ♯ ‘ ∅ ) < ( ♯ ‘ ( 1 ... 𝑛 ) ) ↔ ∅ ≺ ( 1 ... 𝑛 ) ) )
54 6 52 53 mp2an ⊢ ( ( ♯ ‘ ∅ ) < ( ♯ ‘ ( 1 ... 𝑛 ) ) ↔ ∅ ≺ ( 1 ... 𝑛 ) )
55 51 54 sylib ⊢ ( 𝑛 ∈ ℕ → ∅ ≺ ( 1 ... 𝑛 ) )
56 55 anim1i ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( ∅ ≺ ( 1 ... 𝑛 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
57 sdomentr ⊢ ( ( ∅ ≺ ( 1 ... 𝑛 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ∅ ≺ 𝐴 )
58 sdomnen ⊢ ( ∅ ≺ 𝐴 → ¬ ∅ ≈ 𝐴 )
59 57 58 syl ⊢ ( ( ∅ ≺ ( 1 ... 𝑛 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ¬ ∅ ≈ 𝐴 )
60 en0r ⊢ ( ∅ ≈ 𝐴 ↔ 𝐴 = ∅ )
61 60 notbii ⊢ ( ¬ ∅ ≈ 𝐴 ↔ ¬ 𝐴 = ∅ )
62 59 61 sylib ⊢ ( ( ∅ ≺ ( 1 ... 𝑛 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ¬ 𝐴 = ∅ )
63 56 62 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ¬ 𝐴 = ∅ )
64 48 anim1i ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
65 63 64 jca ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
66 44 65 impbii ⊢ ( ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
67 66 exbii ⊢ ( ∃ 𝑛 ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
68 19.42v ⊢ ( ∃ 𝑛 ( ¬ 𝐴 = ∅ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ( ¬ 𝐴 = ∅ ∧ ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) )
69 15 67 68 3bitr2ri ⊢ ( ( ¬ 𝐴 = ∅ ∧ ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ) ↔ ∃ 𝑛 ∈ ℕ ( 1 ... 𝑛 ) ≈ 𝐴 )
70 14 69 bitri ⊢ ( ( ¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ↔ ∃ 𝑛 ∈ ℕ ( 1 ... 𝑛 ) ≈ 𝐴 )
71 10 70 orbi12i ⊢ ( ( ( 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ∨ ( ¬ 𝐴 = ∅ ∧ 𝐴 ∈ Fin ) ) ↔ ( 𝐴 = ∅ ∨ ∃ 𝑛 ∈ ℕ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
72 4 71 bitri ⊢ ( 𝐴 ∈ Fin ↔ ( 𝐴 = ∅ ∨ ∃ 𝑛 ∈ ℕ ( 1 ... 𝑛 ) ≈ 𝐴 ) )