sornom - Metamath Proof Explorer

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

Theorem sornom 8674

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 998	. 2 $/\$ $\/$ $/\$
2		fvelrnb 5920	. . . . . 6
3		fvelrnb 5920	. . . . . 6
4	2, 3	anbi12d 710	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 1017	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 3025	. . . . 5 $/\$ $/\$
7		nnord 6707	. . . . . . . . . . 11
8		nnord 6707	. . . . . . . . . . 11
9		ordtri2or2 4983	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 477	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 466	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 3112	. . . . . . . . . . 11
13		vex 3112	. . . . . . . . . . 11
14		eleq1 2529	. . . . . . . . . . . . . 14
15		eleq1 2529	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 873	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 703	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3522	. . . . . . . . . . . . 13 $/\$
19		fveq2 5872	. . . . . . . . . . . . . . 15
20		fveq2 5872	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4471	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2480	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 709	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 320	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 320	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5872	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4468	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2471	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5872	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4468	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2471	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5872	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4468	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2471	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5872	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4468	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2471	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 709	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 316	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2457	. . . . . . . . . . . . . . . . 17
47	46	olci 391	. . . . . . . . . . . . . . . 16 $\/$
48	47	a1ii 27	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 1003	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 4952	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4469	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2479	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 709	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3208	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 6719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4821	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 802	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 392	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 615	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4459	. . . . . . . . . . . . . . . . . . . . . . . . 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 4460	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2472	. . . . . . . . . . . . . . . . . . . . . . 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 1156	. . . . . . . . . . . . . . . . . 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 6726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 805	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 430	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 615	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 3162	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2529	. . . . . . . . . . . . . . 15
100		eleq1 2529	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 873	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3522	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5872	. . . . . . . . . . . . . . . 16
105		fveq2 5872	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4471	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2480	. . . . . . . . . . . . . . 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 3162	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
112	111	ancom2s 802	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
113	98, 112	orim12d 838	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
114	11, 113	mpd 15	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
115		3mix1 1165	. . . . . . . . . 10 $\/$ $\/$
116		3mix2 1166	. . . . . . . . . 10 $\/$ $\/$
117	115, 116	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
118		3mix3 1167	. . . . . . . . . 10 $\/$ $\/$
119	116	eqcoms 2469	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 379	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 379	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 16	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4461	. . . . . . . 8 $/\$
124		eqeq12 2476	. . . . . . . 8 $/\$
125		breq12 4461	. . . . . . . . 9 $/\$
126	125	ancoms 453	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1298	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 220	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2956	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 218	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 215	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2877	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4810	. 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 972 $/\$ w3a 973

wceq 1395

wcel 1819

wral 2807

wrex 2808

wss 3471 class class class wbr 4456

wpo 4807

wor 4808

word 4886

csuc 4889

crn 5009

wfn 5589

cfv 5594

com 6699

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pr 4695 ax-un 6591

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 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 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 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-iota 5557 df-fun 5596 df-fn 5597 df-fv 5602 df-om 6700

This theorem is referenced by: fin23lem40 8748

W3C validator