Metamath Proof Explorer

Theorem sornom

Description: The range of a single-step monotone function from _om into a partially ordered set is a chain. (Contributed by Stefan O'Rear, 3-Nov-2014)

Ref Expression
Assertion sornom 
|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Or ran F )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Po ran F )
2 fvelrnb 
 |-  ( F Fn _om -> ( b e. ran F <-> E. d e. _om ( F ` d ) = b ) )
3 fvelrnb 
 |-  ( F Fn _om -> ( c e. ran F <-> E. e e. _om ( F ` e ) = c ) )
4 2 3 anbi12d 
 |-  ( F Fn _om -> ( ( b e. ran F /\ c e. ran F ) <-> ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) ) )
5 4 3ad2ant1 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( b e. ran F /\ c e. ran F ) <-> ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) ) )
6 reeanv 
 |-  ( E. d e. _om E. e e. _om ( ( F ` d ) = b /\ ( F ` e ) = c ) <-> ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) )
7 nnord 
 |-  ( d e. _om -> Ord d )
8 nnord 
 |-  ( e e. _om -> Ord e )
9 ordtri2or2 
 |-  ( ( Ord d /\ Ord e ) -> ( d C_ e \/ e C_ d ) )
10 7 8 9 syl2an 
 |-  ( ( d e. _om /\ e e. _om ) -> ( d C_ e \/ e C_ d ) )
11 10 adantl 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( d C_ e \/ e C_ d ) )
12 vex 
 |-  d e. _V
13 vex 
 |-  e e. _V
14 eleq1w 
 |-  ( b = d -> ( b e. _om <-> d e. _om ) )
15 eleq1w 
 |-  ( c = e -> ( c e. _om <-> e e. _om ) )
16 14 15 bi2anan9 
 |-  ( ( b = d /\ c = e ) -> ( ( b e. _om /\ c e. _om ) <-> ( d e. _om /\ e e. _om ) ) )
17 16 anbi2d 
 |-  ( ( b = d /\ c = e ) -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) ) )
18 sseq12 
 |-  ( ( b = d /\ c = e ) -> ( b C_ c <-> d C_ e ) )
19 fveq2 
 |-  ( b = d -> ( F ` b ) = ( F ` d ) )
20 fveq2 
 |-  ( c = e -> ( F ` c ) = ( F ` e ) )
21 19 20 breqan12d 
 |-  ( ( b = d /\ c = e ) -> ( ( F ` b ) R ( F ` c ) <-> ( F ` d ) R ( F ` e ) ) )
22 19 20 eqeqan12d 
 |-  ( ( b = d /\ c = e ) -> ( ( F ` b ) = ( F ` c ) <-> ( F ` d ) = ( F ` e ) ) )
23 21 22 orbi12d 
 |-  ( ( b = d /\ c = e ) -> ( ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) <-> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) )
24 18 23 imbi12d 
 |-  ( ( b = d /\ c = e ) -> ( ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) <-> ( d C_ e -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) ) )
25 17 24 imbi12d 
 |-  ( ( b = d /\ c = e ) -> ( ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) -> ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) ) <-> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( d C_ e -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) ) ) )
26 fveq2 
 |-  ( d = b -> ( F ` d ) = ( F ` b ) )
27 26 breq2d 
 |-  ( d = b -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` b ) ) )
28 26 eqeq2d 
 |-  ( d = b -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` b ) ) )
29 27 28 orbi12d 
 |-  ( d = b -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) ) ) )
30 29 imbi2d 
 |-  ( d = b -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) ) ) ) )
31 fveq2 
 |-  ( d = e -> ( F ` d ) = ( F ` e ) )
32 31 breq2d 
 |-  ( d = e -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` e ) ) )
33 31 eqeq2d 
 |-  ( d = e -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` e ) ) )
34 32 33 orbi12d 
 |-  ( d = e -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) ) )
35 34 imbi2d 
 |-  ( d = e -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) ) ) )
36 fveq2 
 |-  ( d = suc e -> ( F ` d ) = ( F ` suc e ) )
37 36 breq2d 
 |-  ( d = suc e -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` suc e ) ) )
38 36 eqeq2d 
 |-  ( d = suc e -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` suc e ) ) )
39 37 38 orbi12d 
 |-  ( d = suc e -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
40 39 imbi2d 
 |-  ( d = suc e -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
41 fveq2 
 |-  ( d = c -> ( F ` d ) = ( F ` c ) )
42 41 breq2d 
 |-  ( d = c -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` c ) ) )
43 41 eqeq2d 
 |-  ( d = c -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` c ) ) )
44 42 43 orbi12d 
 |-  ( d = c -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
45 44 imbi2d 
 |-  ( d = c -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) ) )
46 eqid 
 |-  ( F ` b ) = ( F ` b )
47 46 olci 
 |-  ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) )
48 47 2a1i 
 |-  ( b e. _om -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) ) ) )
49 fveq2 
 |-  ( a = e -> ( F ` a ) = ( F ` e ) )
50 suceq 
 |-  ( a = e -> suc a = suc e )
51 50 fveq2d 
 |-  ( a = e -> ( F ` suc a ) = ( F ` suc e ) )
52 49 51 breq12d 
 |-  ( a = e -> ( ( F ` a ) R ( F ` suc a ) <-> ( F ` e ) R ( F ` suc e ) ) )
53 49 51 eqeq12d 
 |-  ( a = e -> ( ( F ` a ) = ( F ` suc a ) <-> ( F ` e ) = ( F ` suc e ) ) )
54 52 53 orbi12d 
 |-  ( a = e -> ( ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) <-> ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) ) )
55 simpr2 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) )
56 simplll 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> e e. _om )
57 54 55 56 rspcdva 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) )
58 simprr 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> R Po ran F )
59 simprl 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> F Fn _om )
60 simpllr 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> b e. _om )
61 fnfvelrn 
 |-  ( ( F Fn _om /\ b e. _om ) -> ( F ` b ) e. ran F )
62 59 60 61 syl2anc 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( F ` b ) e. ran F )
63 simplll 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> e e. _om )
64 fnfvelrn 
 |-  ( ( F Fn _om /\ e e. _om ) -> ( F ` e ) e. ran F )
65 59 63 64 syl2anc 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( F ` e ) e. ran F )
66 peano2 
 |-  ( e e. _om -> suc e e. _om )
67 66 ad3antrrr 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> suc e e. _om )
68 fnfvelrn 
 |-  ( ( F Fn _om /\ suc e e. _om ) -> ( F ` suc e ) e. ran F )
69 59 67 68 syl2anc 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( F ` suc e ) e. ran F )
70 potr 
 |-  ( ( R Po ran F /\ ( ( F ` b ) e. ran F /\ ( F ` e ) e. ran F /\ ( F ` suc e ) e. ran F ) ) -> ( ( ( F ` b ) R ( F ` e ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( F ` b ) R ( F ` suc e ) ) )
71 58 62 65 69 70 syl13anc 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( ( F ` b ) R ( F ` e ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( F ` b ) R ( F ` suc e ) ) )
72 71 imp 
 |-  ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( ( F ` b ) R ( F ` e ) /\ ( F ` e ) R ( F ` suc e ) ) ) -> ( F ` b ) R ( F ` suc e ) )
73 72 ancom2s 
 |-  ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( ( F ` e ) R ( F ` suc e ) /\ ( F ` b ) R ( F ` e ) ) ) -> ( F ` b ) R ( F ` suc e ) )
74 73 orcd 
 |-  ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( ( F ` e ) R ( F ` suc e ) /\ ( F ` b ) R ( F ` e ) ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) )
75 74 expr 
 |-  ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( ( F ` b ) R ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
76 breq1 
 |-  ( ( F ` b ) = ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) <-> ( F ` e ) R ( F ` suc e ) ) )
77 76 biimprcd 
 |-  ( ( F ` e ) R ( F ` suc e ) -> ( ( F ` b ) = ( F ` e ) -> ( F ` b ) R ( F ` suc e ) ) )
78 orc 
 |-  ( ( F ` b ) R ( F ` suc e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) )
79 77 78 syl6 
 |-  ( ( F ` e ) R ( F ` suc e ) -> ( ( F ` b ) = ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
80 79 adantl 
 |-  ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( ( F ` b ) = ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
81 75 80 jaod 
 |-  ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
82 81 ex 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( F ` e ) R ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
83 breq2 
 |-  ( ( F ` e ) = ( F ` suc e ) -> ( ( F ` b ) R ( F ` e ) <-> ( F ` b ) R ( F ` suc e ) ) )
84 eqeq2 
 |-  ( ( F ` e ) = ( F ` suc e ) -> ( ( F ` b ) = ( F ` e ) <-> ( F ` b ) = ( F ` suc e ) ) )
85 83 84 orbi12d 
 |-  ( ( F ` e ) = ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) <-> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
86 85 biimpd 
 |-  ( ( F ` e ) = ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
87 86 a1i 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( F ` e ) = ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
88 82 87 jaod 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
89 88 3adantr2 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> ( ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
90 57 89 mpd 
 |-  ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
91 90 ex 
 |-  ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
92 91 a2d 
 |-  ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
93 30 35 40 45 48 92 findsg 
 |-  ( ( ( c e. _om /\ b e. _om ) /\ b C_ c ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
94 93 ancom1s 
 |-  ( ( ( b e. _om /\ c e. _om ) /\ b C_ c ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
95 94 impcom 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( ( b e. _om /\ c e. _om ) /\ b C_ c ) ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) )
96 95 expr 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) -> ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
97 12 13 25 96 vtocl2 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( d C_ e -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) )
98 eleq1w 
 |-  ( b = e -> ( b e. _om <-> e e. _om ) )
99 eleq1w 
 |-  ( c = d -> ( c e. _om <-> d e. _om ) )
100 98 99 bi2anan9 
 |-  ( ( b = e /\ c = d ) -> ( ( b e. _om /\ c e. _om ) <-> ( e e. _om /\ d e. _om ) ) )
101 100 anbi2d 
 |-  ( ( b = e /\ c = d ) -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( e e. _om /\ d e. _om ) ) ) )
102 sseq12 
 |-  ( ( b = e /\ c = d ) -> ( b C_ c <-> e C_ d ) )
103 fveq2 
 |-  ( b = e -> ( F ` b ) = ( F ` e ) )
104 fveq2 
 |-  ( c = d -> ( F ` c ) = ( F ` d ) )
105 103 104 breqan12d 
 |-  ( ( b = e /\ c = d ) -> ( ( F ` b ) R ( F ` c ) <-> ( F ` e ) R ( F ` d ) ) )
106 103 104 eqeqan12d 
 |-  ( ( b = e /\ c = d ) -> ( ( F ` b ) = ( F ` c ) <-> ( F ` e ) = ( F ` d ) ) )
107 105 106 orbi12d 
 |-  ( ( b = e /\ c = d ) -> ( ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) <-> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
108 102 107 imbi12d 
 |-  ( ( b = e /\ c = d ) -> ( ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) <-> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) ) )
109 101 108 imbi12d 
 |-  ( ( b = e /\ c = d ) -> ( ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) -> ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) ) <-> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( e e. _om /\ d e. _om ) ) -> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) ) ) )
110 13 12 109 96 vtocl2 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( e e. _om /\ d e. _om ) ) -> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
111 110 ancom2s 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
112 97 111 orim12d 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( d C_ e \/ e C_ d ) -> ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) \/ ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) ) )
113 11 112 mpd 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) \/ ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
114 3mix1 
 |-  ( ( F ` d ) R ( F ` e ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
115 3mix2 
 |-  ( ( F ` d ) = ( F ` e ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
116 114 115 jaoi 
 |-  ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
117 3mix3 
 |-  ( ( F ` e ) R ( F ` d ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
118 115 eqcoms 
 |-  ( ( F ` e ) = ( F ` d ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
119 117 118 jaoi 
 |-  ( ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
120 116 119 jaoi 
 |-  ( ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) \/ ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
121 113 120 syl 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
122 breq12 
 |-  ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( F ` d ) R ( F ` e ) <-> b R c ) )
123 eqeq12 
 |-  ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( F ` d ) = ( F ` e ) <-> b = c ) )
124 breq12 
 |-  ( ( ( F ` e ) = c /\ ( F ` d ) = b ) -> ( ( F ` e ) R ( F ` d ) <-> c R b ) )
125 124 ancoms 
 |-  ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( F ` e ) R ( F ` d ) <-> c R b ) )
126 122 123 125 3orbi123d 
 |-  ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) <-> ( b R c \/ b = c \/ c R b ) ) )
127 121 126 syl5ibcom 
 |-  ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( b R c \/ b = c \/ c R b ) ) )
128 127 rexlimdvva 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( E. d e. _om E. e e. _om ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( b R c \/ b = c \/ c R b ) ) )
129 6 128 syl5bir 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) -> ( b R c \/ b = c \/ c R b ) ) )
130 5 129 sylbid 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( b e. ran F /\ c e. ran F ) -> ( b R c \/ b = c \/ c R b ) ) )
131 130 ralrimivv 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> A. b e. ran F A. c e. ran F ( b R c \/ b = c \/ c R b ) )
132 df-so 
 |-  ( R Or ran F <-> ( R Po ran F /\ A. b e. ran F A. c e. ran F ( b R c \/ b = c \/ c R b ) ) )
133 1 131 132 sylanbrc 
 |-  ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Or ran F )