Theorem sornom 10355

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 1156	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2		fvelrnb 6945	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏))
3		fvelrnb 6945	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
4	2, 3	anbi12d 644	. . . . 5 ⊢ (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
5	4	3ad2ant1 1151	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
6		reeanv 3234	. . . . 5 ⊢ (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
7		nnord 7885	. . . . . . . . . . 11 ⊢ (𝑑 ∈ ω → Ord 𝑑)
8		nnord 7885	. . . . . . . . . . 11 ⊢ (𝑒 ∈ ω → Ord 𝑒)
9		ordtri2or2 6464	. . . . . . . . . . 11 ⊢ ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
10	7, 8, 9	syl2an 608	. . . . . . . . . 10 ⊢ ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
11	10	adantl 487	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
12		vex 3454	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
13		vex 3454	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
14		eleq1w 2843	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15		eleq1w 2843	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
16	14, 15	bi2anan9 650	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
17	16	anbi2d 642	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18		sseq12 3935	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (𝑏 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑒))
19		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
20		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (𝐹‘𝑐) = (𝐹‘𝑒))
21	19, 20	breqan12d 5118	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑒)))
22	19, 20	eqeqan12d 2774	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑑) = (𝐹‘𝑒)))
23	21, 22	orbi12d 932	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))
24	18, 23	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)))))
25	17, 24	imbi12d 347	. . . . . . . . . . 11 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))))
26		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝐹‘𝑑) = (𝐹‘𝑏))
27	26	breq2d 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑏)))
28	26	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑏)))
29	27, 28	orbi12d 932	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
30	29	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)))))
31		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑒 → (𝐹‘𝑑) = (𝐹‘𝑒))
32	31	breq2d 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑒)))
33	31	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑒)))
34	32, 33	orbi12d 932	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))))
35	34	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)))))
36		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = suc 𝑒 → (𝐹‘𝑑) = (𝐹‘suc 𝑒))
37	36	breq2d 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
38	36	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
39	37, 38	orbi12d 932	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = suc 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
40	39	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
41		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
42	41	breq2d 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑐)))
43	41	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑐)))
44	42, 43	orbi12d 932	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
45	44	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))))
46		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑏) = (𝐹‘𝑏)
47	46	olci 880	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))
48	47	2a1i 12	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
49		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘𝑎) = (𝐹‘𝑒))
50		suceq 6431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
51	50	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
52	49, 51	breq12d 5115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
53	49, 51	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
54	52, 53	orbi12d 932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑒 → (((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒))))
55		simpr2 1214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)))
56		simplll 787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
57	54, 55, 56	rspcdva 3577	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
58		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
59		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
60		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
61		fnfvelrn 7080	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹‘𝑏) ∈ ran 𝐹)
62	59, 60, 61	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑏) ∈ ran 𝐹)
63		simplll 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
64		fnfvelrn 7080	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹‘𝑒) ∈ ran 𝐹)
65	59, 63, 64	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑒) ∈ ran 𝐹)
66		peano2 7901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 ∈ ω → suc 𝑒 ∈ ω)
67	66	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
68		fnfvelrn 7080	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
69	59, 67, 68	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
70		potr 5571	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po ran 𝐹 ∧ ((𝐹‘𝑏) ∈ ran 𝐹 ∧ (𝐹‘𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
71	58, 62, 65, 69, 70	syl13anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
72	71	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
73	72	ancom2s 663	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
74	73	orcd 887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
75	74	expr 462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
76		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
77	76	biimprcd 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
78		orc 881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
79	77, 78	syl6 36	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
80	79	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
81	75, 80	jaod 873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
82	81	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
83		breq2 5106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
84		eqeq2 2772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
85	83, 84	orbi12d 932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
86	85	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
88	82, 87	jaod 873	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
89	88	3adantr2 1189	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
90	57, 89	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
91	90	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
92	91	a2d 30	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
93	30, 35, 40, 45, 48, 92	findsg 7909	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
94	93	ancom1s 666	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
95	94	impcom 413	. . . . . . . . . . . 12 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))
96	95	expr 462	. . . . . . . . . . 11 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
97	12, 13, 25, 96	vtocl2 3526	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))
98		eleq1w 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
99		eleq1w 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
100	98, 99	bi2anan9 650	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
101	100	anbi2d 642	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
102		sseq12 3935	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (𝑏 ⊆ 𝑐 ↔ 𝑒 ⊆ 𝑑))
103		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝐹‘𝑏) = (𝐹‘𝑒))
104		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑑 → (𝐹‘𝑐) = (𝐹‘𝑑))
105	103, 104	breqan12d 5118	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
106	103, 104	eqeqan12d 2774	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑒) = (𝐹‘𝑑)))
107	105, 106	orbi12d 932	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
108	102, 107	imbi12d 347	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
109	101, 108	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))))
110	13, 12, 109, 96	vtocl2 3526	. . . . . . . . . . 11 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
111	110	ancom2s 663	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
112	97, 111	orim12d 979	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
113	11, 112	mpd 16	. . . . . . . 8 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
114		3mix1 1349	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
115		3mix2 1350	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑) = (𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
116	114, 115	jaoi 871	. . . . . . . . 9 ⊢ (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
117		3mix3 1351	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
118	115	eqcoms 2768	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒) = (𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
119	117, 118	jaoi 871	. . . . . . . . 9 ⊢ (((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
120	116, 119	jaoi 871	. . . . . . . 8 ⊢ ((((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
121	113, 120	syl 18	. . . . . . 7 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
122		breq12 5107	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ↔ 𝑏𝑅𝑐))
123		eqeq12 2777	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑) = (𝐹‘𝑒) ↔ 𝑏 = 𝑐))
124		breq12 5107	. . . . . . . . 9 ⊢ (((𝐹‘𝑒) = 𝑐 ∧ (𝐹‘𝑑) = 𝑏) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
125	124	ancoms 464	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
126	122, 123, 125	3orbi123d 1463	. . . . . . 7 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)) ↔ (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
127	121, 126	syl5ibcom 248	. . . . . 6 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
128	127	rexlimdvva 3219	. . . . 5 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
129	6, 128	biimtrrid 246	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
130	5, 129	sylbid 243	. . 3 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
131	130	ralrimivv 3203	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))
132		df-so 5559	. 2 ⊢ (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
133	1, 131, 132	sylanbrc 595	1 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   ⊆ wss 3895   class class class wbr 5102   Po wpo 5556   Or wor 5557  ran crn 5651  Ord word 6361  suc csuc 6364   Fn wfn 6533  ‘cfv 6538  ωcom 7877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546  df-om 7878

This theorem is used by:  fin23lem40  10429