# Metamath Proof Explorer

## Theorem isf32lem2

Description: Lemma for isfin3-2 . Non-minimum implies that there is always another decrease. (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 )`
Assertion isf32lem2
`|- ( ( ph /\ A e. _om ) -> E. a e. _om ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) )`

### 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 )`
` |-  ( ( ph /\ A e. _om ) -> -. |^| ran F e. ran F )`
5 1 ffnd
` |-  ( ph -> F Fn _om )`
6 peano2
` |-  ( A e. _om -> suc A e. _om )`
7 fnfvelrn
` |-  ( ( F Fn _om /\ suc A e. _om ) -> ( F ` suc A ) e. ran F )`
8 5 6 7 syl2an
` |-  ( ( ph /\ A e. _om ) -> ( F ` suc A ) e. ran F )`
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> ( F ` suc A ) e. ran F )`
10 intss1
` |-  ( ( F ` suc A ) e. ran F -> |^| ran F C_ ( F ` suc A ) )`
11 9 10 syl
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> |^| ran F C_ ( F ` suc A ) )`
12 fvelrnb
` |-  ( F Fn _om -> ( b e. ran F <-> E. c e. _om ( F ` c ) = b ) )`
13 5 12 syl
` |-  ( ph -> ( b e. ran F <-> E. c e. _om ( F ` c ) = b ) )`
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> ( b e. ran F <-> E. c e. _om ( F ` c ) = b ) )`
15 simplrr
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ suc A C_ c ) -> c e. _om )`
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ suc A C_ c ) -> suc A e. _om )`
17 simpr
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ suc A C_ c ) -> suc A C_ c )`
18 simplrl
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ suc A C_ c ) -> A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) )`
19 fveq2
` |-  ( b = suc A -> ( F ` b ) = ( F ` suc A ) )`
20 19 eqeq2d
` |-  ( b = suc A -> ( ( F ` suc A ) = ( F ` b ) <-> ( F ` suc A ) = ( F ` suc A ) ) )`
21 20 imbi2d
` |-  ( b = suc A -> ( ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` b ) ) <-> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` suc A ) ) ) )`
22 fveq2
` |-  ( b = d -> ( F ` b ) = ( F ` d ) )`
23 22 eqeq2d
` |-  ( b = d -> ( ( F ` suc A ) = ( F ` b ) <-> ( F ` suc A ) = ( F ` d ) ) )`
24 23 imbi2d
` |-  ( b = d -> ( ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` b ) ) <-> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` d ) ) ) )`
25 fveq2
` |-  ( b = suc d -> ( F ` b ) = ( F ` suc d ) )`
26 25 eqeq2d
` |-  ( b = suc d -> ( ( F ` suc A ) = ( F ` b ) <-> ( F ` suc A ) = ( F ` suc d ) ) )`
27 26 imbi2d
` |-  ( b = suc d -> ( ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` b ) ) <-> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` suc d ) ) ) )`
28 fveq2
` |-  ( b = c -> ( F ` b ) = ( F ` c ) )`
29 28 eqeq2d
` |-  ( b = c -> ( ( F ` suc A ) = ( F ` b ) <-> ( F ` suc A ) = ( F ` c ) ) )`
30 29 imbi2d
` |-  ( b = c -> ( ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` b ) ) <-> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` c ) ) ) )`
31 eqid
` |-  ( F ` suc A ) = ( F ` suc A )`
32 31 2a1i
` |-  ( suc A e. _om -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` suc A ) ) )`
33 elex
` |-  ( suc A e. _om -> suc A e. _V )`
34 sucexb
` |-  ( A e. _V <-> suc A e. _V )`
35 33 34 sylibr
` |-  ( suc A e. _om -> A e. _V )`
` |-  ( ( d e. _om /\ suc A e. _om ) -> A e. _V )`
37 sucssel
` |-  ( A e. _V -> ( suc A C_ d -> A e. d ) )`
38 36 37 syl
` |-  ( ( d e. _om /\ suc A e. _om ) -> ( suc A C_ d -> A e. d ) )`
39 38 imp
` |-  ( ( ( d e. _om /\ suc A e. _om ) /\ suc A C_ d ) -> A e. d )`
40 eleq2w
` |-  ( a = d -> ( A e. a <-> A e. d ) )`
41 suceq
` |-  ( a = d -> suc a = suc d )`
42 41 fveq2d
` |-  ( a = d -> ( F ` suc a ) = ( F ` suc d ) )`
43 fveq2
` |-  ( a = d -> ( F ` a ) = ( F ` d ) )`
44 42 43 eqeq12d
` |-  ( a = d -> ( ( F ` suc a ) = ( F ` a ) <-> ( F ` suc d ) = ( F ` d ) ) )`
45 40 44 imbi12d
` |-  ( a = d -> ( ( A e. a -> ( F ` suc a ) = ( F ` a ) ) <-> ( A e. d -> ( F ` suc d ) = ( F ` d ) ) ) )`
46 45 rspcv
` |-  ( d e. _om -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( A e. d -> ( F ` suc d ) = ( F ` d ) ) ) )`
47 46 com23
` |-  ( d e. _om -> ( A e. d -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc d ) = ( F ` d ) ) ) )`
` |-  ( ( ( d e. _om /\ suc A e. _om ) /\ suc A C_ d ) -> ( A e. d -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc d ) = ( F ` d ) ) ) )`
49 39 48 mpd
` |-  ( ( ( d e. _om /\ suc A e. _om ) /\ suc A C_ d ) -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc d ) = ( F ` d ) ) )`
50 eqtr3
` |-  ( ( ( F ` suc A ) = ( F ` d ) /\ ( F ` suc d ) = ( F ` d ) ) -> ( F ` suc A ) = ( F ` suc d ) )`
51 50 expcom
` |-  ( ( F ` suc d ) = ( F ` d ) -> ( ( F ` suc A ) = ( F ` d ) -> ( F ` suc A ) = ( F ` suc d ) ) )`
52 49 51 syl6
` |-  ( ( ( d e. _om /\ suc A e. _om ) /\ suc A C_ d ) -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( ( F ` suc A ) = ( F ` d ) -> ( F ` suc A ) = ( F ` suc d ) ) ) )`
53 52 a2d
` |-  ( ( ( d e. _om /\ suc A e. _om ) /\ suc A C_ d ) -> ( ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` d ) ) -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` suc d ) ) ) )`
54 21 24 27 30 32 53 findsg
` |-  ( ( ( c e. _om /\ suc A e. _om ) /\ suc A C_ c ) -> ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( F ` suc A ) = ( F ` c ) ) )`
55 54 impr
` |-  ( ( ( c e. _om /\ suc A e. _om ) /\ ( suc A C_ c /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) ) -> ( F ` suc A ) = ( F ` c ) )`
56 15 16 17 18 55 syl22anc
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ suc A C_ c ) -> ( F ` suc A ) = ( F ` c ) )`
57 eqimss
` |-  ( ( F ` suc A ) = ( F ` c ) -> ( F ` suc A ) C_ ( F ` c ) )`
58 56 57 syl
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ suc A C_ c ) -> ( F ` suc A ) C_ ( F ` c ) )`
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ c C_ suc A ) -> suc A e. _om )`
60 simplrr
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ c C_ suc A ) -> c e. _om )`
61 simpr
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ c C_ suc A ) -> c C_ suc A )`
62 simplll
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ c C_ suc A ) -> ph )`
63 1 2 3 isf32lem1
` |-  ( ( ( suc A e. _om /\ c e. _om ) /\ ( c C_ suc A /\ ph ) ) -> ( F ` suc A ) C_ ( F ` c ) )`
64 59 60 61 62 63 syl22anc
` |-  ( ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) /\ c C_ suc A ) -> ( F ` suc A ) C_ ( F ` c ) )`
65 nnord
` |-  ( suc A e. _om -> Ord suc A )`
66 6 65 syl
` |-  ( A e. _om -> Ord suc A )`
` |-  ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) -> Ord suc A )`
68 nnord
` |-  ( c e. _om -> Ord c )`
` |-  ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) -> Ord c )`
70 ordtri2or2
` |-  ( ( Ord suc A /\ Ord c ) -> ( suc A C_ c \/ c C_ suc A ) )`
71 67 69 70 syl2anc
` |-  ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) -> ( suc A C_ c \/ c C_ suc A ) )`
72 58 64 71 mpjaodan
` |-  ( ( ( ph /\ A e. _om ) /\ ( A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) /\ c e. _om ) ) -> ( F ` suc A ) C_ ( F ` c ) )`
73 72 anassrs
` |-  ( ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) /\ c e. _om ) -> ( F ` suc A ) C_ ( F ` c ) )`
74 sseq2
` |-  ( ( F ` c ) = b -> ( ( F ` suc A ) C_ ( F ` c ) <-> ( F ` suc A ) C_ b ) )`
75 73 74 syl5ibcom
` |-  ( ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) /\ c e. _om ) -> ( ( F ` c ) = b -> ( F ` suc A ) C_ b ) )`
76 75 rexlimdva
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> ( E. c e. _om ( F ` c ) = b -> ( F ` suc A ) C_ b ) )`
77 14 76 sylbid
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> ( b e. ran F -> ( F ` suc A ) C_ b ) )`
78 77 ralrimiv
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> A. b e. ran F ( F ` suc A ) C_ b )`
79 ssint
` |-  ( ( F ` suc A ) C_ |^| ran F <-> A. b e. ran F ( F ` suc A ) C_ b )`
80 78 79 sylibr
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> ( F ` suc A ) C_ |^| ran F )`
81 11 80 eqssd
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> |^| ran F = ( F ` suc A ) )`
82 81 9 eqeltrd
` |-  ( ( ( ph /\ A e. _om ) /\ A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) ) -> |^| ran F e. ran F )`
83 4 82 mtand
` |-  ( ( ph /\ A e. _om ) -> -. A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) )`
84 rexnal
` |-  ( E. a e. _om -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) <-> -. A. a e. _om ( A e. a -> ( F ` suc a ) = ( F ` a ) ) )`
85 83 84 sylibr
` |-  ( ( ph /\ A e. _om ) -> E. a e. _om -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) )`
86 suceq
` |-  ( x = a -> suc x = suc a )`
87 86 fveq2d
` |-  ( x = a -> ( F ` suc x ) = ( F ` suc a ) )`
88 fveq2
` |-  ( x = a -> ( F ` x ) = ( F ` a ) )`
89 87 88 sseq12d
` |-  ( x = a -> ( ( F ` suc x ) C_ ( F ` x ) <-> ( F ` suc a ) C_ ( F ` a ) ) )`
90 89 cbvralvw
` |-  ( A. x e. _om ( F ` suc x ) C_ ( F ` x ) <-> A. a e. _om ( F ` suc a ) C_ ( F ` a ) )`
91 2 90 sylib
` |-  ( ph -> A. a e. _om ( F ` suc a ) C_ ( F ` a ) )`
` |-  ( ( ph /\ A e. _om ) -> A. a e. _om ( F ` suc a ) C_ ( F ` a ) )`
93 pm4.61
` |-  ( -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) <-> ( A e. a /\ -. ( F ` suc a ) = ( F ` a ) ) )`
94 dfpss2
` |-  ( ( F ` suc a ) C. ( F ` a ) <-> ( ( F ` suc a ) C_ ( F ` a ) /\ -. ( F ` suc a ) = ( F ` a ) ) )`
95 94 simplbi2
` |-  ( ( F ` suc a ) C_ ( F ` a ) -> ( -. ( F ` suc a ) = ( F ` a ) -> ( F ` suc a ) C. ( F ` a ) ) )`
96 95 anim2d
` |-  ( ( F ` suc a ) C_ ( F ` a ) -> ( ( A e. a /\ -. ( F ` suc a ) = ( F ` a ) ) -> ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) ) )`
97 93 96 syl5bi
` |-  ( ( F ` suc a ) C_ ( F ` a ) -> ( -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) ) )`
98 97 ralimi
` |-  ( A. a e. _om ( F ` suc a ) C_ ( F ` a ) -> A. a e. _om ( -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) ) )`
99 rexim
` |-  ( A. a e. _om ( -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) ) -> ( E. a e. _om -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> E. a e. _om ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) ) )`
100 92 98 99 3syl
` |-  ( ( ph /\ A e. _om ) -> ( E. a e. _om -. ( A e. a -> ( F ` suc a ) = ( F ` a ) ) -> E. a e. _om ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) ) )`
101 85 100 mpd
` |-  ( ( ph /\ A e. _om ) -> E. a e. _om ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) )`