Metamath Proof Explorer

Theorem omsmolem

Description: Lemma for omsmo . (Contributed by NM, 30-Nov-2003) (Revised by David Abernethy, 1-Jan-2014)

Ref Expression
Assertion omsmolem 
|- ( y e. _om -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( y = (/) -> ( z e. y <-> z e. (/) ) )
2 fveq2 
 |-  ( y = (/) -> ( F ` y ) = ( F ` (/) ) )
3 2 eleq2d 
 |-  ( y = (/) -> ( ( F ` z ) e. ( F ` y ) <-> ( F ` z ) e. ( F ` (/) ) ) )
4 1 3 imbi12d 
 |-  ( y = (/) -> ( ( z e. y -> ( F ` z ) e. ( F ` y ) ) <-> ( z e. (/) -> ( F ` z ) e. ( F ` (/) ) ) ) )
5 eleq2 
 |-  ( y = w -> ( z e. y <-> z e. w ) )
6 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
7 6 eleq2d 
 |-  ( y = w -> ( ( F ` z ) e. ( F ` y ) <-> ( F ` z ) e. ( F ` w ) ) )
8 5 7 imbi12d 
 |-  ( y = w -> ( ( z e. y -> ( F ` z ) e. ( F ` y ) ) <-> ( z e. w -> ( F ` z ) e. ( F ` w ) ) ) )
9 eleq2 
 |-  ( y = suc w -> ( z e. y <-> z e. suc w ) )
10 fveq2 
 |-  ( y = suc w -> ( F ` y ) = ( F ` suc w ) )
11 10 eleq2d 
 |-  ( y = suc w -> ( ( F ` z ) e. ( F ` y ) <-> ( F ` z ) e. ( F ` suc w ) ) )
12 9 11 imbi12d 
 |-  ( y = suc w -> ( ( z e. y -> ( F ` z ) e. ( F ` y ) ) <-> ( z e. suc w -> ( F ` z ) e. ( F ` suc w ) ) ) )
13 noel 
 |-  -. z e. (/)
14 13 pm2.21i 
 |-  ( z e. (/) -> ( F ` z ) e. ( F ` (/) ) )
15 14 a1i 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. (/) -> ( F ` z ) e. ( F ` (/) ) ) )
16 vex 
 |-  z e. _V
17 16 elsuc 
 |-  ( z e. suc w <-> ( z e. w \/ z = w ) )
18 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
19 suceq 
 |-  ( x = w -> suc x = suc w )
20 19 fveq2d 
 |-  ( x = w -> ( F ` suc x ) = ( F ` suc w ) )
21 18 20 eleq12d 
 |-  ( x = w -> ( ( F ` x ) e. ( F ` suc x ) <-> ( F ` w ) e. ( F ` suc w ) ) )
22 21 rspccva 
 |-  ( ( A. x e. _om ( F ` x ) e. ( F ` suc x ) /\ w e. _om ) -> ( F ` w ) e. ( F ` suc w ) )
23 22 adantll 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) -> ( F ` w ) e. ( F ` suc w ) )
24 peano2b 
 |-  ( w e. _om <-> suc w e. _om )
25 ffvelrn 
 |-  ( ( F : _om --> A /\ suc w e. _om ) -> ( F ` suc w ) e. A )
26 24 25 sylan2b 
 |-  ( ( F : _om --> A /\ w e. _om ) -> ( F ` suc w ) e. A )
27 ssel 
 |-  ( A C_ On -> ( ( F ` suc w ) e. A -> ( F ` suc w ) e. On ) )
28 ontr1 
 |-  ( ( F ` suc w ) e. On -> ( ( ( F ` z ) e. ( F ` w ) /\ ( F ` w ) e. ( F ` suc w ) ) -> ( F ` z ) e. ( F ` suc w ) ) )
29 28 expcomd 
 |-  ( ( F ` suc w ) e. On -> ( ( F ` w ) e. ( F ` suc w ) -> ( ( F ` z ) e. ( F ` w ) -> ( F ` z ) e. ( F ` suc w ) ) ) )
30 26 27 29 syl56 
 |-  ( A C_ On -> ( ( F : _om --> A /\ w e. _om ) -> ( ( F ` w ) e. ( F ` suc w ) -> ( ( F ` z ) e. ( F ` w ) -> ( F ` z ) e. ( F ` suc w ) ) ) ) )
31 30 impl 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ w e. _om ) -> ( ( F ` w ) e. ( F ` suc w ) -> ( ( F ` z ) e. ( F ` w ) -> ( F ` z ) e. ( F ` suc w ) ) ) )
32 31 adantlr 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) -> ( ( F ` w ) e. ( F ` suc w ) -> ( ( F ` z ) e. ( F ` w ) -> ( F ` z ) e. ( F ` suc w ) ) ) )
33 23 32 mpd 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) -> ( ( F ` z ) e. ( F ` w ) -> ( F ` z ) e. ( F ` suc w ) ) )
34 33 imim2d 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) -> ( ( z e. w -> ( F ` z ) e. ( F ` w ) ) -> ( z e. w -> ( F ` z ) e. ( F ` suc w ) ) ) )
35 34 imp 
 |-  ( ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) /\ ( z e. w -> ( F ` z ) e. ( F ` w ) ) ) -> ( z e. w -> ( F ` z ) e. ( F ` suc w ) ) )
36 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
37 36 eleq1d 
 |-  ( z = w -> ( ( F ` z ) e. ( F ` suc w ) <-> ( F ` w ) e. ( F ` suc w ) ) )
38 22 37 syl5ibrcom 
 |-  ( ( A. x e. _om ( F ` x ) e. ( F ` suc x ) /\ w e. _om ) -> ( z = w -> ( F ` z ) e. ( F ` suc w ) ) )
39 38 ad4ant23 
 |-  ( ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) /\ ( z e. w -> ( F ` z ) e. ( F ` w ) ) ) -> ( z = w -> ( F ` z ) e. ( F ` suc w ) ) )
40 35 39 jaod 
 |-  ( ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) /\ ( z e. w -> ( F ` z ) e. ( F ` w ) ) ) -> ( ( z e. w \/ z = w ) -> ( F ` z ) e. ( F ` suc w ) ) )
41 17 40 syl5bi 
 |-  ( ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ w e. _om ) /\ ( z e. w -> ( F ` z ) e. ( F ` w ) ) ) -> ( z e. suc w -> ( F ` z ) e. ( F ` suc w ) ) )
42 41 exp31 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( w e. _om -> ( ( z e. w -> ( F ` z ) e. ( F ` w ) ) -> ( z e. suc w -> ( F ` z ) e. ( F ` suc w ) ) ) ) )
43 42 com12 
 |-  ( w e. _om -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( ( z e. w -> ( F ` z ) e. ( F ` w ) ) -> ( z e. suc w -> ( F ` z ) e. ( F ` suc w ) ) ) ) )
44 4 8 12 15 43 finds2 
 |-  ( y e. _om -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) ) )