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 
|- ( A e. Fin <-> ( A = (/) \/ E. n e. NN ( 1 ... n ) ~~ A ) )

Proof

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