sornom - Metamath Proof Explorer

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

Theorem sornom 8646

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 993	. 2 $/\$ $\/$ $/\$
2		fvelrnb 5906	. . . . . 6
3		fvelrnb 5906	. . . . . 6
4	2, 3	anbi12d 710	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 1012	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 3022	. . . . 5 $/\$ $/\$
7		nnord 6679	. . . . . . . . . . 11
8		nnord 6679	. . . . . . . . . . 11
9		ordtri2or2 4967	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 477	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 466	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 3109	. . . . . . . . . . 11
13		vex 3109	. . . . . . . . . . 11
14		eleq1 2532	. . . . . . . . . . . . . 14
15		eleq1 2532	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 869	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 703	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3520	. . . . . . . . . . . . 13 $/\$
19		fveq2 5857	. . . . . . . . . . . . . . 15
20		fveq2 5857	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4455	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2483	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 709	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 320	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 320	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5857	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4452	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2474	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5857	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4452	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2474	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5857	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4452	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2474	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5857	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4452	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2474	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2460	. . . . . . . . . . . . . . . . 17
47	46	olci 391	. . . . . . . . . . . . . . . 16 $\/$
48	47	a1ii 27	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 757	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 998	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 4936	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4453	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2482	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 709	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3205	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 6691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 800	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 392	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 615	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . . 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 4444	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2475	. . . . . . . . . . . . . . . . . . . . . . 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 1151	. . . . . . . . . . . . . . . . . 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 6698	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 803	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 430	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 615	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 3159	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2532	. . . . . . . . . . . . . . 15
100		eleq1 2532	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 869	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3520	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5857	. . . . . . . . . . . . . . . 16
105		fveq2 5857	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4455	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2483	. . . . . . . . . . . . . . 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 3159	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
112	111	ancom2s 800	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
113	98, 112	orim12d 835	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
114	11, 113	mpd 15	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
115		3mix1 1160	. . . . . . . . . 10 $\/$ $\/$
116		3mix2 1161	. . . . . . . . . 10 $\/$ $\/$
117	115, 116	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
118		3mix3 1162	. . . . . . . . . 10 $\/$ $\/$
119	116	eqcoms 2472	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 379	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 16	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4445	. . . . . . . 8 $/\$
124		eqeq12 2479	. . . . . . . 8 $/\$
125		breq12 4445	. . . . . . . . 9 $/\$
126	125	ancoms 453	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1293	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 220	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2955	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 218	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 215	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2877	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4794	. 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 967 $/\$ w3a 968

wceq 1374

wcel 1762

wral 2807

wrex 2808

wss 3469 class class class wbr 4440

wpo 4791

wor 4792

word 4870

csuc 4873

crn 4993

wfn 5574

cfv 5579

com 6671

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-sep 4561 ax-nul 4569 ax-pr 4679 ax-un 6567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3108 df-sbc 3325 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-iota 5542 df-fun 5581 df-fn 5582 df-fv 5587 df-om 6672

This theorem is referenced by: fin23lem40 8720

W3C validator