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 ω \land \forall a \in ω (F (a) R F (suc a) \lor F (a) = F (suc a)) \land R Po ran F) \to R Or ran F$

Proof

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

Metamath Proof Explorer

Theorem sornom

Proof