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 8712

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 1011	. 2 $/\$ $\/$ $/\$
2		fvelrnb 5917	. . . . . 6
3		fvelrnb 5917	. . . . . 6
4	2, 3	anbi12d 718	. . . . 5 $/\$ $/\$
5	4	3ad2ant1 1030	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$
6		reeanv 2960	. . . . 5 $/\$ $/\$
7		nnord 6705	. . . . . . . . . . 11
8		nnord 6705	. . . . . . . . . . 11
9		ordtri2or2 5522	. . . . . . . . . . 11 $/\$ $\/$
10	7, 8, 9	syl2an 480	. . . . . . . . . 10 $/\$ $\/$
11	10	adantl 468	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
12		vex 3050	. . . . . . . . . . 11
13		vex 3050	. . . . . . . . . . 11
14		eleq1 2519	. . . . . . . . . . . . . 14
15		eleq1 2519	. . . . . . . . . . . . . 14
16	14, 15	bi2anan9 885	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
17	16	anbi2d 711	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
18		sseq12 3457	. . . . . . . . . . . . 13 $/\$
19		fveq2 5870	. . . . . . . . . . . . . . 15
20		fveq2 5870	. . . . . . . . . . . . . . 15
21	19, 20	breqan12d 4421	. . . . . . . . . . . . . 14 $/\$
22	19, 20	eqeqan12d 2469	. . . . . . . . . . . . . 14 $/\$
23	21, 22	orbi12d 717	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
24	18, 23	imbi12d 322	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
25	17, 24	imbi12d 322	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
26		fveq2 5870	. . . . . . . . . . . . . . . . . 18
27	26	breq2d 4417	. . . . . . . . . . . . . . . . 17
28	26	eqeq2d 2463	. . . . . . . . . . . . . . . . 17
29	27, 28	orbi12d 717	. . . . . . . . . . . . . . . 16 $\/$ $\/$
30	29	imbi2d 318	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
31		fveq2 5870	. . . . . . . . . . . . . . . . . 18
32	31	breq2d 4417	. . . . . . . . . . . . . . . . 17
33	31	eqeq2d 2463	. . . . . . . . . . . . . . . . 17
34	32, 33	orbi12d 717	. . . . . . . . . . . . . . . 16 $\/$ $\/$
35	34	imbi2d 318	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
36		fveq2 5870	. . . . . . . . . . . . . . . . . 18
37	36	breq2d 4417	. . . . . . . . . . . . . . . . 17
38	36	eqeq2d 2463	. . . . . . . . . . . . . . . . 17
39	37, 38	orbi12d 717	. . . . . . . . . . . . . . . 16 $\/$ $\/$
40	39	imbi2d 318	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
41		fveq2 5870	. . . . . . . . . . . . . . . . . 18
42	41	breq2d 4417	. . . . . . . . . . . . . . . . 17
43	41	eqeq2d 2463	. . . . . . . . . . . . . . . . 17
44	42, 43	orbi12d 717	. . . . . . . . . . . . . . . 16 $\/$ $\/$
45	44	imbi2d 318	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
46		eqid 2453	. . . . . . . . . . . . . . . . 17
47	46	olci 393	. . . . . . . . . . . . . . . 16 $\/$
48	47	2a1i 12	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$
49		simplll 769	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
50		simpr2 1016	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
51		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . 22
52		suceq 5491	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . 22
54	51, 53	breq12d 4418	. . . . . . . . . . . . . . . . . . . . 21
55	51, 53	eqeq12d 2468	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	orbi12d 717	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
57	56	rspcva 3150	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $\/$
58	49, 50, 57	syl2anc 667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
59		simprr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
60		simprl 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
61		simpllr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
62		fnfvelrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
63	60, 61, 62	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
64		simplll 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
65		fnfvelrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	60, 64, 65	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
67		peano2 6718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
69		fnfvelrn 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	60, 68, 69	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
71		potr 4770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
72	59, 63, 66, 70, 71	syl13anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	ancom2s 812	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	orcd 394	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
76	75	expr 620	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
77		breq1 4408	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	biimprcd 229	. . . . . . . . . . . . . . . . . . . . . . . 24
79		orc 387	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
80	78, 79	syl6 34	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
81	80	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
82	76, 81	jaod 382	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
83	82	ex 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
84		breq2 4409	. . . . . . . . . . . . . . . . . . . . . . 23
85		eqeq2 2464	. . . . . . . . . . . . . . . . . . . . . . 23
86	84, 85	orbi12d 717	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $\/$
87	86	biimpd 211	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
89	83, 88	jaod 382	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
90	89	3adantr2 1169	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$
91	58, 90	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
92	91	ex 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$
93	92	a2d 29	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
94	30, 35, 40, 45, 48, 93	findsg 6725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
95	94	ancom1s 815	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
96	95	impcom 432	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
97	96	expr 620	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
98	12, 13, 25, 97	vtocl2 3104	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
99		eleq1 2519	. . . . . . . . . . . . . . 15
100		eleq1 2519	. . . . . . . . . . . . . . 15
101	99, 100	bi2anan9 885	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102	101	anbi2d 711	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$
103		sseq12 3457	. . . . . . . . . . . . . 14 $/\$
104		fveq2 5870	. . . . . . . . . . . . . . . 16
105		fveq2 5870	. . . . . . . . . . . . . . . 16
106	104, 105	breqan12d 4421	. . . . . . . . . . . . . . 15 $/\$
107	104, 105	eqeqan12d 2469	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	orbi12d 717	. . . . . . . . . . . . . 14 $/\$ $\/$ $\/$
109	103, 108	imbi12d 322	. . . . . . . . . . . . 13 $/\$ $\/$ $\/$
110	102, 109	imbi12d 322	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
111	13, 12, 110, 97	vtocl2 3104	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
112	111	ancom2s 812	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
113	98, 112	orim12d 850	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
114	11, 113	mpd 15	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
115		3mix1 1178	. . . . . . . . . 10 $\/$ $\/$
116		3mix2 1179	. . . . . . . . . 10 $\/$ $\/$
117	115, 116	jaoi 381	. . . . . . . . 9 $\/$ $\/$ $\/$
118		3mix3 1180	. . . . . . . . . 10 $\/$ $\/$
119	116	eqcoms 2461	. . . . . . . . . 10 $\/$ $\/$
120	118, 119	jaoi 381	. . . . . . . . 9 $\/$ $\/$ $\/$
121	117, 120	jaoi 381	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
122	114, 121	syl 17	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
123		breq12 4410	. . . . . . . 8 $/\$
124		eqeq12 2466	. . . . . . . 8 $/\$
125		breq12 4410	. . . . . . . . 9 $/\$
126	125	ancoms 455	. . . . . . . 8 $/\$
127	123, 124, 126	3orbi123d 1340	. . . . . . 7 $/\$ $\/$ $\/$ $\/$ $\/$
128	122, 127	syl5ibcom 224	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
129	128	rexlimdvva 2888	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
130	6, 129	syl5bir 222	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
131	5, 130	sylbid 219	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
132	131	ralrimivv 2810	. 2 $/\$ $\/$ $/\$ $\/$ $\/$
133		df-so 4759	. 2 $/\$ $\/$ $\/$
134	1, 132, 133	sylanbrc 671	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $\/$ w3o 985 $/\$ w3a 986

wceq 1446

wcel 1889

wral 2739

wrex 2740

wss 3406 class class class wbr 4405

wpo 4756

wor 4757

crn 4838

word 5425

csuc 5428

wfn 5580

cfv 5585

com 6697

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-sbc 3270 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-fv 5593 df-om 6698

This theorem is referenced by: fin23lem40 8786

W3C validator