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 )
4 3 adantr 
 |-  ( ( 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 )
9 8 adantr 
 |-  ( ( ( 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 ) )
14 13 ad2antrr 
 |-  ( ( ( 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 )
16 6 ad3antlr 
 |-  ( ( ( ( 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 )
36 35 adantl 
 |-  ( ( 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 ) ) ) )
48 47 ad2antrr 
 |-  ( ( ( 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 ) )
59 6 ad3antlr 
 |-  ( ( ( ( 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 )
67 66 ad2antlr 
 |-  ( ( ( 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 )
69 68 ad2antll 
 |-  ( ( ( 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 ) )
92 91 adantr 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 ) ) )