sornom - Metamath Proof Explorer

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

Theorem sornom 8438

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 990	. 2 $/\$ $\/$ $/\$
2		fvelrnb 5734	. . . . . 6
3		fvelrnb 5734	. . . . . 6
4	2, 3	anbi12d 710	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 1009	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 2883	. . . . 5 $/\$ $/\$
7		nnord 6479	. . . . . . . . . . 11
8		nnord 6479	. . . . . . . . . . 11
9		ordtri2or2 4810	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 477	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 466	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 2970	. . . . . . . . . . 11
13		vex 2970	. . . . . . . . . . 11
14		eleq1 2498	. . . . . . . . . . . . . 14
15		eleq1 2498	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 868	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 703	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3374	. . . . . . . . . . . . 13 $/\$
19		fveq2 5686	. . . . . . . . . . . . . . 15
20		fveq2 5686	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4302	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2453	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 709	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 320	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 320	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5686	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4299	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2449	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5686	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4299	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2449	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5686	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4299	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2449	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5686	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4299	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2449	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2438	. . . . . . . . . . . . . . . . 17
47	46	olci 391	. . . . . . . . . . . . . . . 16 $\/$
48	47	a1ii 27	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 757	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 995	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 4779	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4300	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2452	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 709	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3066	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 6491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 800	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 392	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 615	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4290	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	biimprcd 225	. . . . . . . . . . . . . . . . . . . . . . . 24
79		orc 385	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
80	78, 79	syl6 33	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
81	80	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
82	76, 81	jaod 380	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
83	82	ex 434	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
84		breq2 4291	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2447	. . . . . . . . . . . . . . . . . . . . . . 23
86	84, 85	orbi12d 709	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $\/$
87	86	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
89	83, 88	jaod 380	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
90	89	3adantr2 1148	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$
91	58, 90	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
92	91	ex 434	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
93	92	a2d 26	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
94	30, 35, 40, 45, 48, 93	findsg 6498	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 803	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 430	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 615	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 3020	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2498	. . . . . . . . . . . . . . 15
100		eleq1 2498	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 868	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3374	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5686	. . . . . . . . . . . . . . . 16
105		fveq2 5686	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4302	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2453	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	orbi12d 709	. . . . . . . . . . . . . 14 $/\$ $\/$ $\/$
109	103, 108	imbi12d 320	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
110	102, 109	imbi12d 320	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
111	13, 12, 110, 97	vtocl2 3020	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
112	111	ancom2s 800	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
113	98, 112	orim12d 834	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
114	11, 113	mpd 15	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
115		3mix1 1157	. . . . . . . . . 10 $\/$ $\/$
116		3mix2 1158	. . . . . . . . . 10 $\/$ $\/$
117	115, 116	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
118		3mix3 1159	. . . . . . . . . 10 $\/$ $\/$
119	116	eqcoms 2441	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 379	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 16	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4292	. . . . . . . 8 $/\$
124		eqeq12 2450	. . . . . . . 8 $/\$
125		breq12 4292	. . . . . . . . 9 $/\$
126	125	ancoms 453	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1288	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 220	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2843	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 218	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 215	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2802	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4637	. 2 $/\$ $\/$ $\/$
134	1, 132, 133	sylanbrc 664	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 964 $/\$ w3a 965

wceq 1369

wcel 1756

wral 2710

wrex 2711

wss 3323 class class class wbr 4287

wpo 4634

wor 4635

word 4713

csuc 4716

crn 4836

wfn 5408

cfv 5413

com 6471

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-sep 4408 ax-nul 4416 ax-pr 4526 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-rab 2719 df-v 2969 df-sbc 3182 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-iota 5376 df-fun 5415 df-fn 5416 df-fv 5421 df-om 6472

This theorem is referenced by: fin23lem40 8512

W3C validator