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 FFnωaωFaRFsucaFa=FsucaRPoranFROrranF

Proof

Step Hyp Ref Expression
1 simp3 FFnωaωFaRFsucaFa=FsucaRPoranFRPoranF
2 fvelrnb FFnωbranFdωFd=b
3 fvelrnb FFnωcranFeωFe=c
4 2 3 anbi12d FFnωbranFcranFdωFd=beωFe=c
5 4 3ad2ant1 FFnωaωFaRFsucaFa=FsucaRPoranFbranFcranFdωFd=beωFe=c
6 reeanv dωeωFd=bFe=cdωFd=beωFe=c
7 nnord dωOrdd
8 nnord eωOrde
9 ordtri2or2 OrddOrdedeed
10 7 8 9 syl2an dωeωdeed
11 10 adantl FFnωaωFaRFsucaFa=FsucaRPoranFdωeωdeed
12 vex dV
13 vex eV
14 eleq1w b=dbωdω
15 eleq1w c=ecωeω
16 14 15 bi2anan9 b=dc=ebωcωdωeω
17 16 anbi2d b=dc=eFFnωaωFaRFsucaFa=FsucaRPoranFbωcωFFnωaωFaRFsucaFa=FsucaRPoranFdωeω
18 sseq12 b=dc=ebcde
19 fveq2 b=dFb=Fd
20 fveq2 c=eFc=Fe
21 19 20 breqan12d b=dc=eFbRFcFdRFe
22 19 20 eqeqan12d b=dc=eFb=FcFd=Fe
23 21 22 orbi12d b=dc=eFbRFcFb=FcFdRFeFd=Fe
24 18 23 imbi12d b=dc=ebcFbRFcFb=FcdeFdRFeFd=Fe
25 17 24 imbi12d b=dc=eFFnωaωFaRFsucaFa=FsucaRPoranFbωcωbcFbRFcFb=FcFFnωaωFaRFsucaFa=FsucaRPoranFdωeωdeFdRFeFd=Fe
26 fveq2 d=bFd=Fb
27 26 breq2d d=bFbRFdFbRFb
28 26 eqeq2d d=bFb=FdFb=Fb
29 27 28 orbi12d d=bFbRFdFb=FdFbRFbFb=Fb
30 29 imbi2d d=bFFnωaωFaRFsucaFa=FsucaRPoranFFbRFdFb=FdFFnωaωFaRFsucaFa=FsucaRPoranFFbRFbFb=Fb
31 fveq2 d=eFd=Fe
32 31 breq2d d=eFbRFdFbRFe
33 31 eqeq2d d=eFb=FdFb=Fe
34 32 33 orbi12d d=eFbRFdFb=FdFbRFeFb=Fe
35 34 imbi2d d=eFFnωaωFaRFsucaFa=FsucaRPoranFFbRFdFb=FdFFnωaωFaRFsucaFa=FsucaRPoranFFbRFeFb=Fe
36 fveq2 d=suceFd=Fsuce
37 36 breq2d d=suceFbRFdFbRFsuce
38 36 eqeq2d d=suceFb=FdFb=Fsuce
39 37 38 orbi12d d=suceFbRFdFb=FdFbRFsuceFb=Fsuce
40 39 imbi2d d=suceFFnωaωFaRFsucaFa=FsucaRPoranFFbRFdFb=FdFFnωaωFaRFsucaFa=FsucaRPoranFFbRFsuceFb=Fsuce
41 fveq2 d=cFd=Fc
42 41 breq2d d=cFbRFdFbRFc
43 41 eqeq2d d=cFb=FdFb=Fc
44 42 43 orbi12d d=cFbRFdFb=FdFbRFcFb=Fc
45 44 imbi2d d=cFFnωaωFaRFsucaFa=FsucaRPoranFFbRFdFb=FdFFnωaωFaRFsucaFa=FsucaRPoranFFbRFcFb=Fc
46 eqid Fb=Fb
47 46 olci FbRFbFb=Fb
48 47 2a1i bωFFnωaωFaRFsucaFa=FsucaRPoranFFbRFbFb=Fb
49 fveq2 a=eFa=Fe
50 suceq a=esuca=suce
51 50 fveq2d a=eFsuca=Fsuce
52 49 51 breq12d a=eFaRFsucaFeRFsuce
53 49 51 eqeq12d a=eFa=FsucaFe=Fsuce
54 52 53 orbi12d a=eFaRFsucaFa=FsucaFeRFsuceFe=Fsuce
55 simpr2 eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFaωFaRFsucaFa=Fsuca
56 simplll eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFeω
57 54 55 56 rspcdva eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFFeRFsuceFe=Fsuce
58 simprr eωbωbeFFnωRPoranFRPoranF
59 simprl eωbωbeFFnωRPoranFFFnω
60 simpllr eωbωbeFFnωRPoranFbω
61 fnfvelrn FFnωbωFbranF
62 59 60 61 syl2anc eωbωbeFFnωRPoranFFbranF
63 simplll eωbωbeFFnωRPoranFeω
64 fnfvelrn FFnωeωFeranF
65 59 63 64 syl2anc eωbωbeFFnωRPoranFFeranF
66 peano2 eωsuceω
67 66 ad3antrrr eωbωbeFFnωRPoranFsuceω
68 fnfvelrn FFnωsuceωFsuceranF
69 59 67 68 syl2anc eωbωbeFFnωRPoranFFsuceranF
70 potr RPoranFFbranFFeranFFsuceranFFbRFeFeRFsuceFbRFsuce
71 58 62 65 69 70 syl13anc eωbωbeFFnωRPoranFFbRFeFeRFsuceFbRFsuce
72 71 imp eωbωbeFFnωRPoranFFbRFeFeRFsuceFbRFsuce
73 72 ancom2s eωbωbeFFnωRPoranFFeRFsuceFbRFeFbRFsuce
74 73 orcd eωbωbeFFnωRPoranFFeRFsuceFbRFeFbRFsuceFb=Fsuce
75 74 expr eωbωbeFFnωRPoranFFeRFsuceFbRFeFbRFsuceFb=Fsuce
76 breq1 Fb=FeFbRFsuceFeRFsuce
77 76 biimprcd FeRFsuceFb=FeFbRFsuce
78 orc FbRFsuceFbRFsuceFb=Fsuce
79 77 78 syl6 FeRFsuceFb=FeFbRFsuceFb=Fsuce
80 79 adantl eωbωbeFFnωRPoranFFeRFsuceFb=FeFbRFsuceFb=Fsuce
81 75 80 jaod eωbωbeFFnωRPoranFFeRFsuceFbRFeFb=FeFbRFsuceFb=Fsuce
82 81 ex eωbωbeFFnωRPoranFFeRFsuceFbRFeFb=FeFbRFsuceFb=Fsuce
83 breq2 Fe=FsuceFbRFeFbRFsuce
84 eqeq2 Fe=FsuceFb=FeFb=Fsuce
85 83 84 orbi12d Fe=FsuceFbRFeFb=FeFbRFsuceFb=Fsuce
86 85 biimpd Fe=FsuceFbRFeFb=FeFbRFsuceFb=Fsuce
87 86 a1i eωbωbeFFnωRPoranFFe=FsuceFbRFeFb=FeFbRFsuceFb=Fsuce
88 82 87 jaod eωbωbeFFnωRPoranFFeRFsuceFe=FsuceFbRFeFb=FeFbRFsuceFb=Fsuce
89 88 3adantr2 eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFFeRFsuceFe=FsuceFbRFeFb=FeFbRFsuceFb=Fsuce
90 57 89 mpd eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFFbRFeFb=FeFbRFsuceFb=Fsuce
91 90 ex eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFFbRFeFb=FeFbRFsuceFb=Fsuce
92 91 a2d eωbωbeFFnωaωFaRFsucaFa=FsucaRPoranFFbRFeFb=FeFFnωaωFaRFsucaFa=FsucaRPoranFFbRFsuceFb=Fsuce
93 30 35 40 45 48 92 findsg cωbωbcFFnωaωFaRFsucaFa=FsucaRPoranFFbRFcFb=Fc
94 93 ancom1s bωcωbcFFnωaωFaRFsucaFa=FsucaRPoranFFbRFcFb=Fc
95 94 impcom FFnωaωFaRFsucaFa=FsucaRPoranFbωcωbcFbRFcFb=Fc
96 95 expr FFnωaωFaRFsucaFa=FsucaRPoranFbωcωbcFbRFcFb=Fc
97 12 13 25 96 vtocl2 FFnωaωFaRFsucaFa=FsucaRPoranFdωeωdeFdRFeFd=Fe
98 eleq1w b=ebωeω
99 eleq1w c=dcωdω
100 98 99 bi2anan9 b=ec=dbωcωeωdω
101 100 anbi2d b=ec=dFFnωaωFaRFsucaFa=FsucaRPoranFbωcωFFnωaωFaRFsucaFa=FsucaRPoranFeωdω
102 sseq12 b=ec=dbced
103 fveq2 b=eFb=Fe
104 fveq2 c=dFc=Fd
105 103 104 breqan12d b=ec=dFbRFcFeRFd
106 103 104 eqeqan12d b=ec=dFb=FcFe=Fd
107 105 106 orbi12d b=ec=dFbRFcFb=FcFeRFdFe=Fd
108 102 107 imbi12d b=ec=dbcFbRFcFb=FcedFeRFdFe=Fd
109 101 108 imbi12d b=ec=dFFnωaωFaRFsucaFa=FsucaRPoranFbωcωbcFbRFcFb=FcFFnωaωFaRFsucaFa=FsucaRPoranFeωdωedFeRFdFe=Fd
110 13 12 109 96 vtocl2 FFnωaωFaRFsucaFa=FsucaRPoranFeωdωedFeRFdFe=Fd
111 110 ancom2s FFnωaωFaRFsucaFa=FsucaRPoranFdωeωedFeRFdFe=Fd
112 97 111 orim12d FFnωaωFaRFsucaFa=FsucaRPoranFdωeωdeedFdRFeFd=FeFeRFdFe=Fd
113 11 112 mpd FFnωaωFaRFsucaFa=FsucaRPoranFdωeωFdRFeFd=FeFeRFdFe=Fd
114 3mix1 FdRFeFdRFeFd=FeFeRFd
115 3mix2 Fd=FeFdRFeFd=FeFeRFd
116 114 115 jaoi FdRFeFd=FeFdRFeFd=FeFeRFd
117 3mix3 FeRFdFdRFeFd=FeFeRFd
118 115 eqcoms Fe=FdFdRFeFd=FeFeRFd
119 117 118 jaoi FeRFdFe=FdFdRFeFd=FeFeRFd
120 116 119 jaoi FdRFeFd=FeFeRFdFe=FdFdRFeFd=FeFeRFd
121 113 120 syl FFnωaωFaRFsucaFa=FsucaRPoranFdωeωFdRFeFd=FeFeRFd
122 breq12 Fd=bFe=cFdRFebRc
123 eqeq12 Fd=bFe=cFd=Feb=c
124 breq12 Fe=cFd=bFeRFdcRb
125 124 ancoms Fd=bFe=cFeRFdcRb
126 122 123 125 3orbi123d Fd=bFe=cFdRFeFd=FeFeRFdbRcb=ccRb
127 121 126 syl5ibcom FFnωaωFaRFsucaFa=FsucaRPoranFdωeωFd=bFe=cbRcb=ccRb
128 127 rexlimdvva FFnωaωFaRFsucaFa=FsucaRPoranFdωeωFd=bFe=cbRcb=ccRb
129 6 128 syl5bir FFnωaωFaRFsucaFa=FsucaRPoranFdωFd=beωFe=cbRcb=ccRb
130 5 129 sylbid FFnωaωFaRFsucaFa=FsucaRPoranFbranFcranFbRcb=ccRb
131 130 ralrimivv FFnωaωFaRFsucaFa=FsucaRPoranFbranFcranFbRcb=ccRb
132 df-so ROrranFRPoranFbranFcranFbRcb=ccRb
133 1 131 132 sylanbrc FFnωaωFaRFsucaFa=FsucaRPoranFROrranF