Metamath Proof Explorer

Theorem onnseq

Description: There are no length _om decreasing sequences in the ordinals. See also noinfep for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015)

Ref Expression
Assertion onnseq 
|- ( ( F ` (/) ) e. On -> E. x e. _om -. ( F ` suc x ) e. ( F ` x ) )

Proof

Step Hyp Ref Expression
1 epweon 
 |-  _E We On
2 fveq2 
 |-  ( y = (/) -> ( F ` y ) = ( F ` (/) ) )
3 2 eleq1d 
 |-  ( y = (/) -> ( ( F ` y ) e. On <-> ( F ` (/) ) e. On ) )
4 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
5 4 eleq1d 
 |-  ( y = z -> ( ( F ` y ) e. On <-> ( F ` z ) e. On ) )
6 fveq2 
 |-  ( y = suc z -> ( F ` y ) = ( F ` suc z ) )
7 6 eleq1d 
 |-  ( y = suc z -> ( ( F ` y ) e. On <-> ( F ` suc z ) e. On ) )
8 simpl 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( F ` (/) ) e. On )
9 suceq 
 |-  ( x = z -> suc x = suc z )
10 9 fveq2d 
 |-  ( x = z -> ( F ` suc x ) = ( F ` suc z ) )
11 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
12 10 11 eleq12d 
 |-  ( x = z -> ( ( F ` suc x ) e. ( F ` x ) <-> ( F ` suc z ) e. ( F ` z ) ) )
13 12 rspcv 
 |-  ( z e. _om -> ( A. x e. _om ( F ` suc x ) e. ( F ` x ) -> ( F ` suc z ) e. ( F ` z ) ) )
14 onelon 
 |-  ( ( ( F ` z ) e. On /\ ( F ` suc z ) e. ( F ` z ) ) -> ( F ` suc z ) e. On )
15 14 expcom 
 |-  ( ( F ` suc z ) e. ( F ` z ) -> ( ( F ` z ) e. On -> ( F ` suc z ) e. On ) )
16 13 15 syl6 
 |-  ( z e. _om -> ( A. x e. _om ( F ` suc x ) e. ( F ` x ) -> ( ( F ` z ) e. On -> ( F ` suc z ) e. On ) ) )
17 16 adantld 
 |-  ( z e. _om -> ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( F ` z ) e. On -> ( F ` suc z ) e. On ) ) )
18 3 5 7 8 17 finds2 
 |-  ( y e. _om -> ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( F ` y ) e. On ) )
19 18 com12 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( y e. _om -> ( F ` y ) e. On ) )
20 19 ralrimiv 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> A. y e. _om ( F ` y ) e. On )
21 eqid 
 |-  ( y e. _om |-> ( F ` y ) ) = ( y e. _om |-> ( F ` y ) )
22 21 fmpt 
 |-  ( A. y e. _om ( F ` y ) e. On <-> ( y e. _om |-> ( F ` y ) ) : _om --> On )
23 20 22 sylib 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( y e. _om |-> ( F ` y ) ) : _om --> On )
24 23 frnd 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ran ( y e. _om |-> ( F ` y ) ) C_ On )
25 peano1 
 |-  (/) e. _om
26 23 fdmd 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> dom ( y e. _om |-> ( F ` y ) ) = _om )
27 25 26 eleqtrrid 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> (/) e. dom ( y e. _om |-> ( F ` y ) ) )
28 27 ne0d 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> dom ( y e. _om |-> ( F ` y ) ) =/= (/) )
29 dm0rn0 
 |-  ( dom ( y e. _om |-> ( F ` y ) ) = (/) <-> ran ( y e. _om |-> ( F ` y ) ) = (/) )
30 29 necon3bii 
 |-  ( dom ( y e. _om |-> ( F ` y ) ) =/= (/) <-> ran ( y e. _om |-> ( F ` y ) ) =/= (/) )
31 28 30 sylib 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ran ( y e. _om |-> ( F ` y ) ) =/= (/) )
32 wefrc 
 |-  ( ( _E We On /\ ran ( y e. _om |-> ( F ` y ) ) C_ On /\ ran ( y e. _om |-> ( F ` y ) ) =/= (/) ) -> E. z e. ran ( y e. _om |-> ( F ` y ) ) ( ran ( y e. _om |-> ( F ` y ) ) i^i z ) = (/) )
33 1 24 31 32 mp3an2i 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> E. z e. ran ( y e. _om |-> ( F ` y ) ) ( ran ( y e. _om |-> ( F ` y ) ) i^i z ) = (/) )
34 fvex 
 |-  ( F ` w ) e. _V
35 34 rgenw 
 |-  A. w e. _om ( F ` w ) e. _V
36 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
37 36 cbvmptv 
 |-  ( y e. _om |-> ( F ` y ) ) = ( w e. _om |-> ( F ` w ) )
38 ineq2 
 |-  ( z = ( F ` w ) -> ( ran ( y e. _om |-> ( F ` y ) ) i^i z ) = ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) )
39 38 eqeq1d 
 |-  ( z = ( F ` w ) -> ( ( ran ( y e. _om |-> ( F ` y ) ) i^i z ) = (/) <-> ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) = (/) ) )
40 37 39 rexrnmptw 
 |-  ( A. w e. _om ( F ` w ) e. _V -> ( E. z e. ran ( y e. _om |-> ( F ` y ) ) ( ran ( y e. _om |-> ( F ` y ) ) i^i z ) = (/) <-> E. w e. _om ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) = (/) ) )
41 35 40 ax-mp 
 |-  ( E. z e. ran ( y e. _om |-> ( F ` y ) ) ( ran ( y e. _om |-> ( F ` y ) ) i^i z ) = (/) <-> E. w e. _om ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) = (/) )
42 33 41 sylib 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> E. w e. _om ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) = (/) )
43 peano2 
 |-  ( w e. _om -> suc w e. _om )
44 43 adantl 
 |-  ( ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) /\ w e. _om ) -> suc w e. _om )
45 eqid 
 |-  ( F ` suc w ) = ( F ` suc w )
46 fveq2 
 |-  ( y = suc w -> ( F ` y ) = ( F ` suc w ) )
47 46 rspceeqv 
 |-  ( ( suc w e. _om /\ ( F ` suc w ) = ( F ` suc w ) ) -> E. y e. _om ( F ` suc w ) = ( F ` y ) )
48 44 45 47 sylancl 
 |-  ( ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) /\ w e. _om ) -> E. y e. _om ( F ` suc w ) = ( F ` y ) )
49 fvex 
 |-  ( F ` suc w ) e. _V
50 21 elrnmpt 
 |-  ( ( F ` suc w ) e. _V -> ( ( F ` suc w ) e. ran ( y e. _om |-> ( F ` y ) ) <-> E. y e. _om ( F ` suc w ) = ( F ` y ) ) )
51 49 50 ax-mp 
 |-  ( ( F ` suc w ) e. ran ( y e. _om |-> ( F ` y ) ) <-> E. y e. _om ( F ` suc w ) = ( F ` y ) )
52 48 51 sylibr 
 |-  ( ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) /\ w e. _om ) -> ( F ` suc w ) e. ran ( y e. _om |-> ( F ` y ) ) )
53 suceq 
 |-  ( x = w -> suc x = suc w )
54 53 fveq2d 
 |-  ( x = w -> ( F ` suc x ) = ( F ` suc w ) )
55 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
56 54 55 eleq12d 
 |-  ( x = w -> ( ( F ` suc x ) e. ( F ` x ) <-> ( F ` suc w ) e. ( F ` w ) ) )
57 56 rspccva 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ w e. _om ) -> ( F ` suc w ) e. ( F ` w ) )
58 57 adantll 
 |-  ( ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) /\ w e. _om ) -> ( F ` suc w ) e. ( F ` w ) )
59 inelcm 
 |-  ( ( ( F ` suc w ) e. ran ( y e. _om |-> ( F ` y ) ) /\ ( F ` suc w ) e. ( F ` w ) ) -> ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) =/= (/) )
60 52 58 59 syl2anc 
 |-  ( ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) /\ w e. _om ) -> ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) =/= (/) )
61 60 neneqd 
 |-  ( ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) /\ w e. _om ) -> -. ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) = (/) )
62 61 nrexdv 
 |-  ( ( ( F ` (/) ) e. On /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> -. E. w e. _om ( ran ( y e. _om |-> ( F ` y ) ) i^i ( F ` w ) ) = (/) )
63 42 62 pm2.65da 
 |-  ( ( F ` (/) ) e. On -> -. A. x e. _om ( F ` suc x ) e. ( F ` x ) )
64 rexnal 
 |-  ( E. x e. _om -. ( F ` suc x ) e. ( F ` x ) <-> -. A. x e. _om ( F ` suc x ) e. ( F ` x ) )
65 63 64 sylibr 
 |-  ( ( F ` (/) ) e. On -> E. x e. _om -. ( F ` suc x ) e. ( F ` x ) )