sornom - Metamath Proof Explorer

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

Theorem sornom 8725

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 1032	. 2 $/\$ $\/$ $/\$
2		fvelrnb 5926	. . . . . 6
3		fvelrnb 5926	. . . . . 6
4	2, 3	anbi12d 725	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 1051	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 2944	. . . . 5 $/\$ $/\$
7		nnord 6719	. . . . . . . . . . 11
8		nnord 6719	. . . . . . . . . . 11
9		ordtri2or2 5526	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 485	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 473	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 3034	. . . . . . . . . . 11
13		vex 3034	. . . . . . . . . . 11
14		eleq1 2537	. . . . . . . . . . . . . 14
15		eleq1 2537	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 890	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 718	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3441	. . . . . . . . . . . . 13 $/\$
19		fveq2 5879	. . . . . . . . . . . . . . 15
20		fveq2 5879	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4411	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2487	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 724	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 327	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 327	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5879	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4407	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2481	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 724	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 323	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5879	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4407	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2481	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 724	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 323	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5879	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4407	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2481	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 724	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 323	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5879	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4407	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2481	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 724	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 323	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2471	. . . . . . . . . . . . . . . . 17
47	46	olci 398	. . . . . . . . . . . . . . . 16 $\/$
48	47	2a1i 12	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 776	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 1037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 5495	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4408	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2486	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 724	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3134	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 673	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 6732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 436	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 819	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 399	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 626	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	biimprcd 233	. . . . . . . . . . . . . . . . . . . . . . . 24
79		orc 392	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
80	78, 79	syl6 33	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
81	80	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
82	76, 81	jaod 387	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
83	82	ex 441	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
84		breq2 4399	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2482	. . . . . . . . . . . . . . . . . . . . . . 23
86	84, 85	orbi12d 724	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $\/$
87	86	biimpd 212	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
89	83, 88	jaod 387	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
90	89	3adantr2 1190	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$
91	58, 90	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
92	91	ex 441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
93	92	a2d 28	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
94	30, 35, 40, 45, 48, 93	findsg 6739	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 822	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 437	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 626	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 3088	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2537	. . . . . . . . . . . . . . 15
100		eleq1 2537	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 890	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 718	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3441	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5879	. . . . . . . . . . . . . . . 16
105		fveq2 5879	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4411	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2487	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	orbi12d 724	. . . . . . . . . . . . . 14 $/\$ $\/$ $\/$
109	103, 108	imbi12d 327	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
110	102, 109	imbi12d 327	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
111	13, 12, 110, 97	vtocl2 3088	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
112	111	ancom2s 819	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
113	98, 112	orim12d 856	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
114	11, 113	mpd 15	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
115		3mix1 1199	. . . . . . . . . 10 $\/$ $\/$
116		3mix2 1200	. . . . . . . . . 10 $\/$ $\/$
117	115, 116	jaoi 386	. . . . . . . . 9 $\/$ $\/$ $\/$
118		3mix3 1201	. . . . . . . . . 10 $\/$ $\/$
119	116	eqcoms 2479	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 386	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 386	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 17	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4400	. . . . . . . 8 $/\$
124		eqeq12 2484	. . . . . . . 8 $/\$
125		breq12 4400	. . . . . . . . 9 $/\$
126	125	ancoms 460	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1364	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 228	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2878	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 226	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 223	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2813	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4761	. 2 $/\$ $\/$ $\/$
134	1, 132, 133	sylanbrc 677	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $\/$ w3o 1006 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756

wrex 2757

wss 3390 class class class wbr 4395

wpo 4758

wor 4759

crn 4840

word 5429

csuc 5432

wfn 5584

cfv 5589

com 6711

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-fv 5597 df-om 6712

This theorem is referenced by: fin23lem40 8799

W3C validator