sornom

Description: The range of a single-step monotone function from _om into a partially ordered set is a chain. (Contributed by Stefan O'Rear, 3-Nov-2014)

		Ref	Expression
	Assertion	sornom	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Or ran F )

Proof

Step	Hyp	Ref	Expression
1		simp3	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Po ran F )
2		fvelrnb	\|- ( F Fn _om -> ( b e. ran F <-> E. d e. _om ( F ` d ) = b ) )
3		fvelrnb	\|- ( F Fn _om -> ( c e. ran F <-> E. e e. _om ( F ` e ) = c ) )
4	2 3	anbi12d	\|- ( F Fn _om -> ( ( b e. ran F /\ c e. ran F ) <-> ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) ) )
5	4	3ad2ant1	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( b e. ran F /\ c e. ran F ) <-> ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) ) )
6		reeanv	\|- ( E. d e. _om E. e e. _om ( ( F ` d ) = b /\ ( F ` e ) = c ) <-> ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) )
7		nnord	\|- ( d e. _om -> Ord d )
8		nnord	\|- ( e e. _om -> Ord e )
9		ordtri2or2	\|- ( ( Ord d /\ Ord e ) -> ( d C_ e \/ e C_ d ) )
10	7 8 9	syl2an	\|- ( ( d e. _om /\ e e. _om ) -> ( d C_ e \/ e C_ d ) )
11	10	adantl	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( d C_ e \/ e C_ d ) )
12		vex	\|- d e. _V
13		vex	\|- e e. _V
14		eleq1w	\|- ( b = d -> ( b e. _om <-> d e. _om ) )
15		eleq1w	\|- ( c = e -> ( c e. _om <-> e e. _om ) )
16	14 15	bi2anan9	\|- ( ( b = d /\ c = e ) -> ( ( b e. _om /\ c e. _om ) <-> ( d e. _om /\ e e. _om ) ) )
17	16	anbi2d	\|- ( ( b = d /\ c = e ) -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) ) )
18		sseq12	\|- ( ( b = d /\ c = e ) -> ( b C_ c <-> d C_ e ) )
19		fveq2	\|- ( b = d -> ( F ` b ) = ( F ` d ) )
20		fveq2	\|- ( c = e -> ( F ` c ) = ( F ` e ) )
21	19 20	breqan12d	\|- ( ( b = d /\ c = e ) -> ( ( F ` b ) R ( F ` c ) <-> ( F ` d ) R ( F ` e ) ) )
22	19 20	eqeqan12d	\|- ( ( b = d /\ c = e ) -> ( ( F ` b ) = ( F ` c ) <-> ( F ` d ) = ( F ` e ) ) )
23	21 22	orbi12d	\|- ( ( b = d /\ c = e ) -> ( ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) <-> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) )
24	18 23	imbi12d	\|- ( ( b = d /\ c = e ) -> ( ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) <-> ( d C_ e -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) ) )
25	17 24	imbi12d	\|- ( ( b = d /\ c = e ) -> ( ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) -> ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) ) <-> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( d C_ e -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) ) ) )
26		fveq2	\|- ( d = b -> ( F ` d ) = ( F ` b ) )
27	26	breq2d	\|- ( d = b -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` b ) ) )
28	26	eqeq2d	\|- ( d = b -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` b ) ) )
29	27 28	orbi12d	\|- ( d = b -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) ) ) )
30	29	imbi2d	\|- ( d = b -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) ) ) ) )
31		fveq2	\|- ( d = e -> ( F ` d ) = ( F ` e ) )
32	31	breq2d	\|- ( d = e -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` e ) ) )
33	31	eqeq2d	\|- ( d = e -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` e ) ) )
34	32 33	orbi12d	\|- ( d = e -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) ) )
35	34	imbi2d	\|- ( d = e -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) ) ) )
36		fveq2	\|- ( d = suc e -> ( F ` d ) = ( F ` suc e ) )
37	36	breq2d	\|- ( d = suc e -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` suc e ) ) )
38	36	eqeq2d	\|- ( d = suc e -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` suc e ) ) )
39	37 38	orbi12d	\|- ( d = suc e -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
40	39	imbi2d	\|- ( d = suc e -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
41		fveq2	\|- ( d = c -> ( F ` d ) = ( F ` c ) )
42	41	breq2d	\|- ( d = c -> ( ( F ` b ) R ( F ` d ) <-> ( F ` b ) R ( F ` c ) ) )
43	41	eqeq2d	\|- ( d = c -> ( ( F ` b ) = ( F ` d ) <-> ( F ` b ) = ( F ` c ) ) )
44	42 43	orbi12d	\|- ( d = c -> ( ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) <-> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
45	44	imbi2d	\|- ( d = c -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` d ) \/ ( F ` b ) = ( F ` d ) ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) ) )
46		eqid	\|- ( F ` b ) = ( F ` b )
47	46	olci	\|- ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) )
48	47	2a1i	\|- ( b e. _om -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` b ) \/ ( F ` b ) = ( F ` b ) ) ) )
49		fveq2	\|- ( a = e -> ( F ` a ) = ( F ` e ) )
50		suceq	\|- ( a = e -> suc a = suc e )
51	50	fveq2d	\|- ( a = e -> ( F ` suc a ) = ( F ` suc e ) )
52	49 51	breq12d	\|- ( a = e -> ( ( F ` a ) R ( F ` suc a ) <-> ( F ` e ) R ( F ` suc e ) ) )
53	49 51	eqeq12d	\|- ( a = e -> ( ( F ` a ) = ( F ` suc a ) <-> ( F ` e ) = ( F ` suc e ) ) )
54	52 53	orbi12d	\|- ( a = e -> ( ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) <-> ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) ) )
55		simpr2	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) )
56		simplll	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> e e. _om )
57	54 55 56	rspcdva	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) )
58		simprr	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> R Po ran F )
59		simprl	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> F Fn _om )
60		simpllr	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> b e. _om )
61		fnfvelrn	\|- ( ( F Fn _om /\ b e. _om ) -> ( F ` b ) e. ran F )
62	59 60 61	syl2anc	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( F ` b ) e. ran F )
63		simplll	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> e e. _om )
64		fnfvelrn	\|- ( ( F Fn _om /\ e e. _om ) -> ( F ` e ) e. ran F )
65	59 63 64	syl2anc	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( F ` e ) e. ran F )
66		peano2	\|- ( e e. _om -> suc e e. _om )
67	66	ad3antrrr	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> suc e e. _om )
68		fnfvelrn	\|- ( ( F Fn _om /\ suc e e. _om ) -> ( F ` suc e ) e. ran F )
69	59 67 68	syl2anc	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( F ` suc e ) e. ran F )
70		potr	\|- ( ( R Po ran F /\ ( ( F ` b ) e. ran F /\ ( F ` e ) e. ran F /\ ( F ` suc e ) e. ran F ) ) -> ( ( ( F ` b ) R ( F ` e ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( F ` b ) R ( F ` suc e ) ) )
71	58 62 65 69 70	syl13anc	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( ( F ` b ) R ( F ` e ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( F ` b ) R ( F ` suc e ) ) )
72	71	imp	\|- ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( ( F ` b ) R ( F ` e ) /\ ( F ` e ) R ( F ` suc e ) ) ) -> ( F ` b ) R ( F ` suc e ) )
73	72	ancom2s	\|- ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( ( F ` e ) R ( F ` suc e ) /\ ( F ` b ) R ( F ` e ) ) ) -> ( F ` b ) R ( F ` suc e ) )
74	73	orcd	\|- ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( ( F ` e ) R ( F ` suc e ) /\ ( F ` b ) R ( F ` e ) ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) )
75	74	expr	\|- ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( ( F ` b ) R ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
76		breq1	\|- ( ( F ` b ) = ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) <-> ( F ` e ) R ( F ` suc e ) ) )
77	76	biimprcd	\|- ( ( F ` e ) R ( F ` suc e ) -> ( ( F ` b ) = ( F ` e ) -> ( F ` b ) R ( F ` suc e ) ) )
78		orc	\|- ( ( F ` b ) R ( F ` suc e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) )
79	77 78	syl6	\|- ( ( F ` e ) R ( F ` suc e ) -> ( ( F ` b ) = ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
80	79	adantl	\|- ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( ( F ` b ) = ( F ` e ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
81	75 80	jaod	\|- ( ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) /\ ( F ` e ) R ( F ` suc e ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
82	81	ex	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( F ` e ) R ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
83		breq2	\|- ( ( F ` e ) = ( F ` suc e ) -> ( ( F ` b ) R ( F ` e ) <-> ( F ` b ) R ( F ` suc e ) ) )
84		eqeq2	\|- ( ( F ` e ) = ( F ` suc e ) -> ( ( F ` b ) = ( F ` e ) <-> ( F ` b ) = ( F ` suc e ) ) )
85	83 84	orbi12d	\|- ( ( F ` e ) = ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) <-> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
86	85	biimpd	\|- ( ( F ` e ) = ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
87	86	a1i	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( F ` e ) = ( F ` suc e ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
88	82 87	jaod	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ R Po ran F ) ) -> ( ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
89	88	3adantr2	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> ( ( ( F ` e ) R ( F ` suc e ) \/ ( F ` e ) = ( F ` suc e ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
90	57 89	mpd	\|- ( ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) /\ ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) )
91	90	ex	\|- ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
92	91	a2d	\|- ( ( ( e e. _om /\ b e. _om ) /\ b C_ e ) -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` e ) \/ ( F ` b ) = ( F ` e ) ) ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` suc e ) \/ ( F ` b ) = ( F ` suc e ) ) ) ) )
93	30 35 40 45 48 92	findsg	\|- ( ( ( c e. _om /\ b e. _om ) /\ b C_ c ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
94	93	ancom1s	\|- ( ( ( b e. _om /\ c e. _om ) /\ b C_ c ) -> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
95	94	impcom	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( ( b e. _om /\ c e. _om ) /\ b C_ c ) ) -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) )
96	95	expr	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) -> ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) )
97	12 13 25 96	vtocl2	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( d C_ e -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) ) )
98		eleq1w	\|- ( b = e -> ( b e. _om <-> e e. _om ) )
99		eleq1w	\|- ( c = d -> ( c e. _om <-> d e. _om ) )
100	98 99	bi2anan9	\|- ( ( b = e /\ c = d ) -> ( ( b e. _om /\ c e. _om ) <-> ( e e. _om /\ d e. _om ) ) )
101	100	anbi2d	\|- ( ( b = e /\ c = d ) -> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) <-> ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( e e. _om /\ d e. _om ) ) ) )
102		sseq12	\|- ( ( b = e /\ c = d ) -> ( b C_ c <-> e C_ d ) )
103		fveq2	\|- ( b = e -> ( F ` b ) = ( F ` e ) )
104		fveq2	\|- ( c = d -> ( F ` c ) = ( F ` d ) )
105	103 104	breqan12d	\|- ( ( b = e /\ c = d ) -> ( ( F ` b ) R ( F ` c ) <-> ( F ` e ) R ( F ` d ) ) )
106	103 104	eqeqan12d	\|- ( ( b = e /\ c = d ) -> ( ( F ` b ) = ( F ` c ) <-> ( F ` e ) = ( F ` d ) ) )
107	105 106	orbi12d	\|- ( ( b = e /\ c = d ) -> ( ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) <-> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
108	102 107	imbi12d	\|- ( ( b = e /\ c = d ) -> ( ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) <-> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) ) )
109	101 108	imbi12d	\|- ( ( b = e /\ c = d ) -> ( ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( b e. _om /\ c e. _om ) ) -> ( b C_ c -> ( ( F ` b ) R ( F ` c ) \/ ( F ` b ) = ( F ` c ) ) ) ) <-> ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( e e. _om /\ d e. _om ) ) -> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) ) ) )
110	13 12 109 96	vtocl2	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( e e. _om /\ d e. _om ) ) -> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
111	110	ancom2s	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( e C_ d -> ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
112	97 111	orim12d	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( d C_ e \/ e C_ d ) -> ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) \/ ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) ) )
113	11 112	mpd	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) \/ ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) )
114		3mix1	\|- ( ( F ` d ) R ( F ` e ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
115		3mix2	\|- ( ( F ` d ) = ( F ` e ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
116	114 115	jaoi	\|- ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
117		3mix3	\|- ( ( F ` e ) R ( F ` d ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
118	115	eqcoms	\|- ( ( F ` e ) = ( F ` d ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
119	117 118	jaoi	\|- ( ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
120	116 119	jaoi	\|- ( ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) ) \/ ( ( F ` e ) R ( F ` d ) \/ ( F ` e ) = ( F ` d ) ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
121	113 120	syl	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) )
122		breq12	\|- ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( F ` d ) R ( F ` e ) <-> b R c ) )
123		eqeq12	\|- ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( F ` d ) = ( F ` e ) <-> b = c ) )
124		breq12	\|- ( ( ( F ` e ) = c /\ ( F ` d ) = b ) -> ( ( F ` e ) R ( F ` d ) <-> c R b ) )
125	124	ancoms	\|- ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( F ` e ) R ( F ` d ) <-> c R b ) )
126	122 123 125	3orbi123d	\|- ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( ( ( F ` d ) R ( F ` e ) \/ ( F ` d ) = ( F ` e ) \/ ( F ` e ) R ( F ` d ) ) <-> ( b R c \/ b = c \/ c R b ) ) )
127	121 126	syl5ibcom	\|- ( ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) /\ ( d e. _om /\ e e. _om ) ) -> ( ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( b R c \/ b = c \/ c R b ) ) )
128	127	rexlimdvva	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( E. d e. _om E. e e. _om ( ( F ` d ) = b /\ ( F ` e ) = c ) -> ( b R c \/ b = c \/ c R b ) ) )
129	6 128	biimtrrid	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( E. d e. _om ( F ` d ) = b /\ E. e e. _om ( F ` e ) = c ) -> ( b R c \/ b = c \/ c R b ) ) )
130	5 129	sylbid	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> ( ( b e. ran F /\ c e. ran F ) -> ( b R c \/ b = c \/ c R b ) ) )
131	130	ralrimivv	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> A. b e. ran F A. c e. ran F ( b R c \/ b = c \/ c R b ) )
132		df-so	\|- ( R Or ran F <-> ( R Po ran F /\ A. b e. ran F A. c e. ran F ( b R c \/ b = c \/ c R b ) ) )
133	1 131 132	sylanbrc	\|- ( ( F Fn _om /\ A. a e. _om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Or ran F )

Metamath Proof Explorer

Theorem sornom

Proof