Theorem sornom 10189

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	⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)

Distinct variable groups:   𝐹,𝑎   𝑅,𝑎

Proof of Theorem sornom

Dummy variables 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 1139	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2		fvelrnb 6893	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏))
3		fvelrnb 6893	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
4	2, 3	anbi12d 633	. . . . 5 ⊢ (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
5	4	3ad2ant1 1134	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
6		reeanv 3207	. . . . 5 ⊢ (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
7		nnord 7816	. . . . . . . . . . 11 ⊢ (𝑑 ∈ ω → Ord 𝑑)
8		nnord 7816	. . . . . . . . . . 11 ⊢ (𝑒 ∈ ω → Ord 𝑒)
9		ordtri2or2 6417	. . . . . . . . . . 11 ⊢ ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
10	7, 8, 9	syl2an 597	. . . . . . . . . 10 ⊢ ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
11	10	adantl 481	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
12		vex 3443	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
13		vex 3443	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
14		eleq1w 2818	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15		eleq1w 2818	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
16	14, 15	bi2anan9 639	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
17	16	anbi2d 631	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18		sseq12 3960	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (𝑏 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑒))
19		fveq2 6833	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
20		fveq2 6833	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (𝐹‘𝑐) = (𝐹‘𝑒))
21	19, 20	breqan12d 5113	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑒)))
22	19, 20	eqeqan12d 2749	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑑) = (𝐹‘𝑒)))
23	21, 22	orbi12d 919	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))
24	18, 23	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)))))
25	17, 24	imbi12d 344	. . . . . . . . . . 11 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))))
26		fveq2 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝐹‘𝑑) = (𝐹‘𝑏))
27	26	breq2d 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑏)))
28	26	eqeq2d 2746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑏)))
29	27, 28	orbi12d 919	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
30	29	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)))))
31		fveq2 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑒 → (𝐹‘𝑑) = (𝐹‘𝑒))
32	31	breq2d 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑒)))
33	31	eqeq2d 2746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑒)))
34	32, 33	orbi12d 919	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))))
35	34	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)))))
36		fveq2 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = suc 𝑒 → (𝐹‘𝑑) = (𝐹‘suc 𝑒))
37	36	breq2d 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
38	36	eqeq2d 2746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
39	37, 38	orbi12d 919	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = suc 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
40	39	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
41		fveq2 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
42	41	breq2d 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑐)))
43	41	eqeq2d 2746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑐)))
44	42, 43	orbi12d 919	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
45	44	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))))
46		eqid 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑏) = (𝐹‘𝑏)
47	46	olci 867	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))
48	47	2a1i 12	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
49		fveq2 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘𝑎) = (𝐹‘𝑒))
50		suceq 6384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
51	50	fveq2d 6837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
52	49, 51	breq12d 5110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
53	49, 51	eqeq12d 2751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
54	52, 53	orbi12d 919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑒 → (((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒))))
55		simpr2 1197	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)))
56		simplll 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
57	54, 55, 56	rspcdva 3576	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
58		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
59		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
60		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
61		fnfvelrn 7025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹‘𝑏) ∈ ran 𝐹)
62	59, 60, 61	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑏) ∈ ran 𝐹)
63		simplll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
64		fnfvelrn 7025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹‘𝑒) ∈ ran 𝐹)
65	59, 63, 64	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑒) ∈ ran 𝐹)
66		peano2 7832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 ∈ ω → suc 𝑒 ∈ ω)
67	66	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
68		fnfvelrn 7025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
69	59, 67, 68	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
70		potr 5544	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po ran 𝐹 ∧ ((𝐹‘𝑏) ∈ ran 𝐹 ∧ (𝐹‘𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
71	58, 62, 65, 69, 70	syl13anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
72	71	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
73	72	ancom2s 651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
74	73	orcd 874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
75	74	expr 456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
76		breq1 5100	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
77	76	biimprcd 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
78		orc 868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
79	77, 78	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
80	79	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
81	75, 80	jaod 860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
82	81	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
83		breq2 5101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
84		eqeq2 2747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
85	83, 84	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
86	85	biimpd 229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
88	82, 87	jaod 860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
89	88	3adantr2 1172	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
90	57, 89	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
91	90	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
92	91	a2d 29	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
93	30, 35, 40, 45, 48, 92	findsg 7839	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
94	93	ancom1s 654	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
95	94	impcom 407	. . . . . . . . . . . 12 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))
96	95	expr 456	. . . . . . . . . . 11 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
97	12, 13, 25, 96	vtocl2 3521	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))
98		eleq1w 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
99		eleq1w 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
100	98, 99	bi2anan9 639	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
101	100	anbi2d 631	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
102		sseq12 3960	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (𝑏 ⊆ 𝑐 ↔ 𝑒 ⊆ 𝑑))
103		fveq2 6833	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝐹‘𝑏) = (𝐹‘𝑒))
104		fveq2 6833	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑑 → (𝐹‘𝑐) = (𝐹‘𝑑))
105	103, 104	breqan12d 5113	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
106	103, 104	eqeqan12d 2749	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑒) = (𝐹‘𝑑)))
107	105, 106	orbi12d 919	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
108	102, 107	imbi12d 344	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
109	101, 108	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))))
110	13, 12, 109, 96	vtocl2 3521	. . . . . . . . . . 11 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
111	110	ancom2s 651	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
112	97, 111	orim12d 967	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
113	11, 112	mpd 15	. . . . . . . 8 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
114		3mix1 1332	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
115		3mix2 1333	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑) = (𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
116	114, 115	jaoi 858	. . . . . . . . 9 ⊢ (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
117		3mix3 1334	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
118	115	eqcoms 2743	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒) = (𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
119	117, 118	jaoi 858	. . . . . . . . 9 ⊢ (((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
120	116, 119	jaoi 858	. . . . . . . 8 ⊢ ((((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
121	113, 120	syl 17	. . . . . . 7 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
122		breq12 5102	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ↔ 𝑏𝑅𝑐))
123		eqeq12 2752	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑) = (𝐹‘𝑒) ↔ 𝑏 = 𝑐))
124		breq12 5102	. . . . . . . . 9 ⊢ (((𝐹‘𝑒) = 𝑐 ∧ (𝐹‘𝑑) = 𝑏) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
125	124	ancoms 458	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
126	122, 123, 125	3orbi123d 1438	. . . . . . 7 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)) ↔ (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
127	121, 126	syl5ibcom 245	. . . . . 6 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
128	127	rexlimdvva 3192	. . . . 5 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
129	6, 128	biimtrrid 243	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
130	5, 129	sylbid 240	. . 3 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
131	130	ralrimivv 3176	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))
132		df-so 5532	. 2 ⊢ (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
133	1, 131, 132	sylanbrc 584	1 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3050  ∃wrex 3059   ⊆ wss 3900   class class class wbr 5097   Po wpo 5529   Or wor 5530  ran crn 5624  Ord word 6315  suc csuc 6318   Fn wfn 6486  ‘cfv 6491  ωcom 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6447  df-fun 6493  df-fn 6494  df-fv 6499  df-om 7809

This theorem is referenced by:  fin23lem40  10263