sornom - Metamath Proof Explorer

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

Theorem sornom 8113

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.

Step	Hyp	Ref	Expression
1		simp3 959	. 2 $/\$ $\/$ $/\$
2		fvelrnb 5733	. . . . . 6
3		fvelrnb 5733	. . . . . 6
4	2, 3	anbi12d 692	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 978	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 2835	. . . . 5 $/\$ $/\$
7		nnord 4812	. . . . . . . . . . 11
8		nnord 4812	. . . . . . . . . . 11
9		ordtri2or2 4637	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 464	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 453	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 2919	. . . . . . . . . . 11
13		vex 2919	. . . . . . . . . . 11
14		eleq1 2464	. . . . . . . . . . . . . 14
15		eleq1 2464	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 844	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 685	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3331	. . . . . . . . . . . . 13 $/\$
19		fveq2 5687	. . . . . . . . . . . . . . 15
20		fveq2 5687	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4187	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2419	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 691	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 312	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 312	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5687	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4184	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2415	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 691	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 308	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5687	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4184	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2415	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 691	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 308	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5687	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4184	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2415	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 691	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 308	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5687	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4184	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2415	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 691	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 308	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2404	. . . . . . . . . . . . . . . . 17
47	46	olci 381	. . . . . . . . . . . . . . . 16 $\/$
48	47	a1ii 25	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 735	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 964	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 4606	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4185	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 691	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3010	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 4824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 778	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 382	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 599	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	biimprcd 217	. . . . . . . . . . . . . . . . . . . . . . . 24
79		orc 375	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
80	78, 79	syl6 31	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
81	80	adantl 453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
82	76, 81	jaod 370	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
83	82	ex 424	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
84		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2413	. . . . . . . . . . . . . . . . . . . . . . 23
86	84, 85	orbi12d 691	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $\/$
87	86	biimpd 199	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
89	83, 88	jaod 370	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
90	89	3adantr2 1117	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$
91	58, 90	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
92	91	ex 424	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
93	92	a2d 24	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
94	30, 35, 40, 45, 48, 93	findsg 4831	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 781	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 420	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 599	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 2967	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2464	. . . . . . . . . . . . . . 15
100		eleq1 2464	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 844	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 685	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3331	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5687	. . . . . . . . . . . . . . . 16
105		fveq2 5687	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4187	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2419	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	orbi12d 691	. . . . . . . . . . . . . 14 $/\$ $\/$ $\/$
109	103, 108	imbi12d 312	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
110	102, 109	imbi12d 312	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
111	13, 12, 110, 97	vtocl2 2967	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
112	111	ancom2s 778	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
113	98, 112	orim12d 812	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
114	11, 113	mpd 15	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
115		3mix1 1126	. . . . . . . . . 10 $\/$ $\/$
116		3mix2 1127	. . . . . . . . . 10 $\/$ $\/$
117	115, 116	jaoi 369	. . . . . . . . 9 $\/$ $\/$ $\/$
118		3mix3 1128	. . . . . . . . . 10 $\/$ $\/$
119	116	eqcoms 2407	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 369	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 369	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 16	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4177	. . . . . . . 8 $/\$
124		eqeq12 2416	. . . . . . . 8 $/\$
125		breq12 4177	. . . . . . . . 9 $/\$
126	125	ancoms 440	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1253	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 212	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2797	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 210	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 207	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2757	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4464	. 2 $/\$ $\/$ $\/$
134	1, 132, 133	sylanbrc 646	1 $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $\/$ w3o 935 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2666

wrex 2667

wss 3280 class class class wbr 4172

wpo 4461

wor 4462

word 4540

csuc 4543

com 4804

crn 4838

wfn 5408

cfv 5413

This theorem is referenced by: fin23lem40 8187

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pr 4363 ax-un 4660

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-rab 2675 df-v 2918 df-sbc 3122 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-iota 5377 df-fun 5415 df-fn 5416 df-fv 5421

W3C validator