MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sornom Unicode version

Theorem sornom 8678
Description: The range of a single-step monotone function from into a partially ordered set is a chain. (Contributed by Stefan O'Rear, 3-Nov-2014.)
Assertion
Ref Expression
sornom
Distinct variable groups:   ,   ,

Proof of Theorem sornom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 998 . 2
2 fvelrnb 5920 . . . . . 6
3 fvelrnb 5920 . . . . . 6
42, 3anbi12d 710 . . . . 5
543ad2ant1 1017 . . . 4
6 reeanv 3025 . . . . 5
7 nnord 6708 . . . . . . . . . . 11
8 nnord 6708 . . . . . . . . . . 11
9 ordtri2or2 4979 . . . . . . . . . . 11
107, 8, 9syl2an 477 . . . . . . . . . 10
1110adantl 466 . . . . . . . . 9
12 vex 3112 . . . . . . . . . . 11
13 vex 3112 . . . . . . . . . . 11
14 eleq1 2529 . . . . . . . . . . . . . 14
15 eleq1 2529 . . . . . . . . . . . . . 14
1614, 15bi2anan9 873 . . . . . . . . . . . . 13
1716anbi2d 703 . . . . . . . . . . . 12
18 sseq12 3526 . . . . . . . . . . . . 13
19 fveq2 5871 . . . . . . . . . . . . . . 15
20 fveq2 5871 . . . . . . . . . . . . . . 15
2119, 20breqan12d 4467 . . . . . . . . . . . . . 14
2219, 20eqeqan12d 2480 . . . . . . . . . . . . . 14
2321, 22orbi12d 709 . . . . . . . . . . . . 13
2418, 23imbi12d 320 . . . . . . . . . . . 12
2517, 24imbi12d 320 . . . . . . . . . . 11
26 fveq2 5871 . . . . . . . . . . . . . . . . . 18
2726breq2d 4464 . . . . . . . . . . . . . . . . 17
2826eqeq2d 2471 . . . . . . . . . . . . . . . . 17
2927, 28orbi12d 709 . . . . . . . . . . . . . . . 16
3029imbi2d 316 . . . . . . . . . . . . . . 15
31 fveq2 5871 . . . . . . . . . . . . . . . . . 18
3231breq2d 4464 . . . . . . . . . . . . . . . . 17
3331eqeq2d 2471 . . . . . . . . . . . . . . . . 17
3432, 33orbi12d 709 . . . . . . . . . . . . . . . 16
3534imbi2d 316 . . . . . . . . . . . . . . 15
36 fveq2 5871 . . . . . . . . . . . . . . . . . 18
3736breq2d 4464 . . . . . . . . . . . . . . . . 17
3836eqeq2d 2471 . . . . . . . . . . . . . . . . 17
3937, 38orbi12d 709 . . . . . . . . . . . . . . . 16
4039imbi2d 316 . . . . . . . . . . . . . . 15
41 fveq2 5871 . . . . . . . . . . . . . . . . . 18
4241breq2d 4464 . . . . . . . . . . . . . . . . 17
4341eqeq2d 2471 . . . . . . . . . . . . . . . . 17
4442, 43orbi12d 709 . . . . . . . . . . . . . . . 16
4544imbi2d 316 . . . . . . . . . . . . . . 15
46 eqid 2457 . . . . . . . . . . . . . . . . 17
4746olci 391 . . . . . . . . . . . . . . . 16
4847a1ii 27 . . . . . . . . . . . . . . 15
49 simplll 759 . . . . . . . . . . . . . . . . . . 19
50 simpr2 1003 . . . . . . . . . . . . . . . . . . 19
51 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
52 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . 23
5352fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . 22
5451, 53breq12d 4465 . . . . . . . . . . . . . . . . . . . . 21
5551, 53eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . 21
5654, 55orbi12d 709 . . . . . . . . . . . . . . . . . . . 20
5756rspcva 3208 . . . . . . . . . . . . . . . . . . 19
5849, 50, 57syl2anc 661 . . . . . . . . . . . . . . . . . 18
59 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
60 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
61 simpllr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62 fnfvelrn 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6360, 61, 62syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
64 simplll 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
65 fnfvelrn 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6660, 64, 65syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
67 peano2 6720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6867ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69 fnfvelrn 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7060, 68, 69syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
71 potr 4817 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7259, 63, 66, 70, 71syl13anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7372imp 429 . . . . . . . . . . . . . . . . . . . . . . . . 25
7473ancom2s 802 . . . . . . . . . . . . . . . . . . . . . . . 24
7574orcd 392 . . . . . . . . . . . . . . . . . . . . . . 23
7675expr 615 . . . . . . . . . . . . . . . . . . . . . 22
77 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . . 25
7877biimprcd 225 . . . . . . . . . . . . . . . . . . . . . . . 24
79 orc 385 . . . . . . . . . . . . . . . . . . . . . . . 24
8078, 79syl6 33 . . . . . . . . . . . . . . . . . . . . . . 23
8180adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
8276, 81jaod 380 . . . . . . . . . . . . . . . . . . . . 21
8382ex 434 . . . . . . . . . . . . . . . . . . . 20
84 breq2 4456 . . . . . . . . . . . . . . . . . . . . . . 23
85 eqeq2 2472 . . . . . . . . . . . . . . . . . . . . . . 23
8684, 85orbi12d 709 . . . . . . . . . . . . . . . . . . . . . 22
8786biimpd 207 . . . . . . . . . . . . . . . . . . . . 21
8887a1i 11 . . . . . . . . . . . . . . . . . . . 20
8983, 88jaod 380 . . . . . . . . . . . . . . . . . . 19
90893adantr2 1156 . . . . . . . . . . . . . . . . . 18
9158, 90mpd 15 . . . . . . . . . . . . . . . . 17
9291ex 434 . . . . . . . . . . . . . . . 16
9392a2d 26 . . . . . . . . . . . . . . 15
9430, 35, 40, 45, 48, 93findsg 6727 . . . . . . . . . . . . . 14
9594ancom1s 805 . . . . . . . . . . . . 13
9695impcom 430 . . . . . . . . . . . 12
9796expr 615 . . . . . . . . . . 11
9812, 13, 25, 97vtocl2 3162 . . . . . . . . . 10
99 eleq1 2529 . . . . . . . . . . . . . . 15
100 eleq1 2529 . . . . . . . . . . . . . . 15
10199, 100bi2anan9 873 . . . . . . . . . . . . . 14
102101anbi2d 703 . . . . . . . . . . . . 13
103 sseq12 3526 . . . . . . . . . . . . . 14
104 fveq2 5871 . . . . . . . . . . . . . . . 16
105 fveq2 5871 . . . . . . . . . . . . . . . 16
106104, 105breqan12d 4467 . . . . . . . . . . . . . . 15
107104, 105eqeqan12d 2480 . . . . . . . . . . . . . . 15
108106, 107orbi12d 709 . . . . . . . . . . . . . 14
109103, 108imbi12d 320 . . . . . . . . . . . . 13
110102, 109imbi12d 320 . . . . . . . . . . . 12
11113, 12, 110, 97vtocl2 3162 . . . . . . . . . . 11
112111ancom2s 802 . . . . . . . . . 10
11398, 112orim12d 838 . . . . . . . . 9
11411, 113mpd 15 . . . . . . . 8
115 3mix1 1165 . . . . . . . . . 10
116 3mix2 1166 . . . . . . . . . 10
117115, 116jaoi 379 . . . . . . . . 9
118 3mix3 1167 . . . . . . . . . 10
119116eqcoms 2469 . . . . . . . . . 10
120118, 119jaoi 379 . . . . . . . . 9
121117, 120jaoi 379 . . . . . . . 8
122114, 121syl 16 . . . . . . 7
123 breq12 4457 . . . . . . . 8
124 eqeq12 2476 . . . . . . . 8
125 breq12 4457 . . . . . . . . 9
126125ancoms 453 . . . . . . . 8
127123, 124, 1263orbi123d 1298 . . . . . . 7
128122, 127syl5ibcom 220 . . . . . 6
129128rexlimdvva 2956 . . . . 5
1306, 129syl5bir 218 . . . 4
1315, 130sylbid 215 . . 3
132131ralrimivv 2877 . 2
133 df-so 4806 . 2
1341, 132, 133sylanbrc 664 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  \/w3o 972  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  C_wss 3475   class class class wbr 4452  Powpo 4803  Orwor 4804  Ordword 4882  succsuc 4885  rancrn 5005  Fnwfn 5588  `cfv 5593   com 6700
This theorem is referenced by:  fin23lem40  8752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785