sornom - Metamath Proof Explorer

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

Theorem sornom 8558

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 5849	. . . . . 6
3		fvelrnb 5849	. . . . . 6
4	2, 3	anbi12d 710	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 1009	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 2994	. . . . 5 $/\$ $/\$
7		nnord 6595	. . . . . . . . . . 11
8		nnord 6595	. . . . . . . . . . 11
9		ordtri2or2 4924	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 477	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 466	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 3081	. . . . . . . . . . 11
13		vex 3081	. . . . . . . . . . 11
14		eleq1 2526	. . . . . . . . . . . . . 14
15		eleq1 2526	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 868	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 703	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3488	. . . . . . . . . . . . 13 $/\$
19		fveq2 5800	. . . . . . . . . . . . . . 15
20		fveq2 5800	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4416	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2477	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 709	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 320	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 320	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5800	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4413	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2468	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5800	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4413	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2468	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5800	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4413	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2468	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5800	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4413	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2468	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2454	. . . . . . . . . . . . . . . . 17
47	46	olci 391	. . . . . . . . . . . . . . . 16 $\/$
48	47	a1ii 27	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 757	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 995	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5800	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 4893	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5804	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4414	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 709	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3177	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 5950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 5950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 6607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 5950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1221	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 800	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 392	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 615	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4404	. . . . . . . . . . . . . . . . . . . . . . . . 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 4405	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2469	. . . . . . . . . . . . . . . . . . . . . . 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 6614	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 803	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 430	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 615	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 3131	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2526	. . . . . . . . . . . . . . 15
100		eleq1 2526	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 868	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3488	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5800	. . . . . . . . . . . . . . . 16
105		fveq2 5800	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4416	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2477	. . . . . . . . . . . . . . 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 3131	. . . . . . . . . . 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 2466	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 379	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 16	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4406	. . . . . . . 8 $/\$
124		eqeq12 2473	. . . . . . . 8 $/\$
125		breq12 4406	. . . . . . . . 9 $/\$
126	125	ancoms 453	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1289	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 220	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2954	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 218	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 215	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2913	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4751	. 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 1370

wcel 1758

wral 2799

wrex 2800

wss 3437 class class class wbr 4401

wpo 4748

wor 4749

word 4827

csuc 4830

crn 4950

wfn 5522

cfv 5527

com 6587

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4522 ax-nul 4530 ax-pr 4640 ax-un 6483

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-rab 2808 df-v 3080 df-sbc 3295 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-tp 3991 df-op 3993 df-uni 4201 df-br 4402 df-opab 4460 df-mpt 4461 df-tr 4495 df-eprel 4741 df-id 4745 df-po 4750 df-so 4751 df-fr 4788 df-we 4790 df-ord 4831 df-on 4832 df-lim 4833 df-suc 4834 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-iota 5490 df-fun 5529 df-fn 5530 df-fv 5535 df-om 6588

This theorem is referenced by: fin23lem40 8632

W3C validator