This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isf32lem5

Description: Lemma for isfin3-2 . There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a 
|- ( ph -> F : _om --> ~P G )
isf32lem.b 
|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
isf32lem.c 
|- ( ph -> -. |^| ran F e. ran F )
isf32lem.d 
|- S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
Assertion isf32lem5 
|- ( ph -> -. S e. Fin )

Proof

Step Hyp Ref Expression
1 isf32lem.a 
 |-  ( ph -> F : _om --> ~P G )
2 isf32lem.b 
 |-  ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
3 isf32lem.c 
 |-  ( ph -> -. |^| ran F e. ran F )
4 isf32lem.d 
 |-  S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
5 1 2 3 isf32lem2 
 |-  ( ( ph /\ a e. _om ) -> E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
6 5 ralrimiva 
 |-  ( ph -> A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
7 4 ssrab3 
 |-  S C_ _om
8 nnunifi 
 |-  ( ( S C_ _om /\ S e. Fin ) -> U. S e. _om )
9 7 8 mpan 
 |-  ( S e. Fin -> U. S e. _om )
10 9 adantl 
 |-  ( ( ph /\ S e. Fin ) -> U. S e. _om )
11 elssuni 
 |-  ( b e. S -> b C_ U. S )
12 nnon 
 |-  ( b e. _om -> b e. On )
13 omsson 
 |-  _om C_ On
14 13 10 sselid 
 |-  ( ( ph /\ S e. Fin ) -> U. S e. On )
15 ontri1 
 |-  ( ( b e. On /\ U. S e. On ) -> ( b C_ U. S <-> -. U. S e. b ) )
16 12 14 15 syl2anr 
 |-  ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( b C_ U. S <-> -. U. S e. b ) )
17 11 16 imbitrid 
 |-  ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( b e. S -> -. U. S e. b ) )
18 17 con2d 
 |-  ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( U. S e. b -> -. b e. S ) )
19 18 impr 
 |-  ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> -. b e. S )
20 4 eleq2i 
 |-  ( b e. S <-> b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } )
21 19 20 sylnib 
 |-  ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> -. b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } )
22 suceq 
 |-  ( y = b -> suc y = suc b )
23 22 fveq2d 
 |-  ( y = b -> ( F ` suc y ) = ( F ` suc b ) )
24 fveq2 
 |-  ( y = b -> ( F ` y ) = ( F ` b ) )
25 23 24 psseq12d 
 |-  ( y = b -> ( ( F ` suc y ) C. ( F ` y ) <-> ( F ` suc b ) C. ( F ` b ) ) )
26 25 elrab3 
 |-  ( b e. _om -> ( b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } <-> ( F ` suc b ) C. ( F ` b ) ) )
27 26 ad2antrl 
 |-  ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> ( b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } <-> ( F ` suc b ) C. ( F ` b ) ) )
28 21 27 mtbid 
 |-  ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> -. ( F ` suc b ) C. ( F ` b ) )
29 28 expr 
 |-  ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( U. S e. b -> -. ( F ` suc b ) C. ( F ` b ) ) )
30 imnan 
 |-  ( ( U. S e. b -> -. ( F ` suc b ) C. ( F ` b ) ) <-> -. ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
31 29 30 sylib 
 |-  ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> -. ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
32 31 nrexdv 
 |-  ( ( ph /\ S e. Fin ) -> -. E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
33 eleq1 
 |-  ( a = U. S -> ( a e. b <-> U. S e. b ) )
34 33 anbi1d 
 |-  ( a = U. S -> ( ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
35 34 rexbidv 
 |-  ( a = U. S -> ( E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
36 35 notbid 
 |-  ( a = U. S -> ( -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> -. E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
37 36 rspcev 
 |-  ( ( U. S e. _om /\ -. E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) -> E. a e. _om -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
38 10 32 37 syl2anc 
 |-  ( ( ph /\ S e. Fin ) -> E. a e. _om -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
39 rexnal 
 |-  ( E. a e. _om -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> -. A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
40 38 39 sylib 
 |-  ( ( ph /\ S e. Fin ) -> -. A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
41 40 ex 
 |-  ( ph -> ( S e. Fin -> -. A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
42 6 41 mt2d 
 |-  ( ph -> -. S e. Fin )