Theorem sornom 10308

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 1135	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2		fvelrnb 6964	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏))
3		fvelrnb 6964	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
4	2, 3	anbi12d 630	. . . . 5 ⊢ (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
5	4	3ad2ant1 1130	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
6		reeanv 3224	. . . . 5 ⊢ (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
7		nnord 7884	. . . . . . . . . . 11 ⊢ (𝑑 ∈ ω → Ord 𝑑)
8		nnord 7884	. . . . . . . . . . 11 ⊢ (𝑒 ∈ ω → Ord 𝑒)
9		ordtri2or2 6473	. . . . . . . . . . 11 ⊢ ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
10	7, 8, 9	syl2an 594	. . . . . . . . . 10 ⊢ ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
11	10	adantl 480	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
12		vex 3477	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
13		vex 3477	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
14		eleq1w 2812	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15		eleq1w 2812	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
16	14, 15	bi2anan9 636	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
17	16	anbi2d 628	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18		sseq12 4009	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (𝑏 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑒))
19		fveq2 6902	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
20		fveq2 6902	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (𝐹‘𝑐) = (𝐹‘𝑒))
21	19, 20	breqan12d 5168	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑒)))
22	19, 20	eqeqan12d 2742	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑑) = (𝐹‘𝑒)))
23	21, 22	orbi12d 916	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))
24	18, 23	imbi12d 343	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)))))
25	17, 24	imbi12d 343	. . . . . . . . . . 11 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))))
26		fveq2 6902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝐹‘𝑑) = (𝐹‘𝑏))
27	26	breq2d 5164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑏)))
28	26	eqeq2d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑏)))
29	27, 28	orbi12d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
30	29	imbi2d 339	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)))))
31		fveq2 6902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑒 → (𝐹‘𝑑) = (𝐹‘𝑒))
32	31	breq2d 5164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑒)))
33	31	eqeq2d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑒)))
34	32, 33	orbi12d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))))
35	34	imbi2d 339	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)))))
36		fveq2 6902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = suc 𝑒 → (𝐹‘𝑑) = (𝐹‘suc 𝑒))
37	36	breq2d 5164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
38	36	eqeq2d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
39	37, 38	orbi12d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = suc 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
40	39	imbi2d 339	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
41		fveq2 6902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
42	41	breq2d 5164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑐)))
43	41	eqeq2d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑐)))
44	42, 43	orbi12d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
45	44	imbi2d 339	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))))
46		eqid 2728	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑏) = (𝐹‘𝑏)
47	46	olci 864	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))
48	47	2a1i 12	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
49		fveq2 6902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘𝑎) = (𝐹‘𝑒))
50		suceq 6440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
51	50	fveq2d 6906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
52	49, 51	breq12d 5165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
53	49, 51	eqeq12d 2744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
54	52, 53	orbi12d 916	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑒 → (((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒))))
55		simpr2 1192	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)))
56		simplll 773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
57	54, 55, 56	rspcdva 3612	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
58		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
59		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
60		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
61		fnfvelrn 7095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹‘𝑏) ∈ ran 𝐹)
62	59, 60, 61	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑏) ∈ ran 𝐹)
63		simplll 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
64		fnfvelrn 7095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹‘𝑒) ∈ ran 𝐹)
65	59, 63, 64	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑒) ∈ ran 𝐹)
66		peano2 7902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 ∈ ω → suc 𝑒 ∈ ω)
67	66	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
68		fnfvelrn 7095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
69	59, 67, 68	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
70		potr 5607	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po ran 𝐹 ∧ ((𝐹‘𝑏) ∈ ran 𝐹 ∧ (𝐹‘𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
71	58, 62, 65, 69, 70	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
72	71	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
73	72	ancom2s 648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
74	73	orcd 871	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
75	74	expr 455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
76		breq1 5155	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
77	76	biimprcd 249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
78		orc 865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
79	77, 78	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
80	79	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
81	75, 80	jaod 857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
82	81	ex 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
83		breq2 5156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
84		eqeq2 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
85	83, 84	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
86	85	biimpd 228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
88	82, 87	jaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
89	88	3adantr2 1167	. . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . 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 7911	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
94	93	ancom1s 651	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
95	94	impcom 406	. . . . . . . . . . . 12 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))
96	95	expr 455	. . . . . . . . . . 11 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
97	12, 13, 25, 96	vtocl2 3554	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))
98		eleq1w 2812	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
99		eleq1w 2812	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
100	98, 99	bi2anan9 636	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
101	100	anbi2d 628	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
102		sseq12 4009	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (𝑏 ⊆ 𝑐 ↔ 𝑒 ⊆ 𝑑))
103		fveq2 6902	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝐹‘𝑏) = (𝐹‘𝑒))
104		fveq2 6902	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑑 → (𝐹‘𝑐) = (𝐹‘𝑑))
105	103, 104	breqan12d 5168	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
106	103, 104	eqeqan12d 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑒) = (𝐹‘𝑑)))
107	105, 106	orbi12d 916	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
108	102, 107	imbi12d 343	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
109	101, 108	imbi12d 343	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))))
110	13, 12, 109, 96	vtocl2 3554	. . . . . . . . . . 11 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
111	110	ancom2s 648	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
112	97, 111	orim12d 962	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
113	11, 112	mpd 15	. . . . . . . 8 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
114		3mix1 1327	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
115		3mix2 1328	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑) = (𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
116	114, 115	jaoi 855	. . . . . . . . 9 ⊢ (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
117		3mix3 1329	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
118	115	eqcoms 2736	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒) = (𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
119	117, 118	jaoi 855	. . . . . . . . 9 ⊢ (((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
120	116, 119	jaoi 855	. . . . . . . 8 ⊢ ((((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
121	113, 120	syl 17	. . . . . . 7 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
122		breq12 5157	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ↔ 𝑏𝑅𝑐))
123		eqeq12 2745	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑) = (𝐹‘𝑒) ↔ 𝑏 = 𝑐))
124		breq12 5157	. . . . . . . . 9 ⊢ (((𝐹‘𝑒) = 𝑐 ∧ (𝐹‘𝑑) = 𝑏) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
125	124	ancoms 457	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
126	122, 123, 125	3orbi123d 1431	. . . . . . 7 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)) ↔ (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
127	121, 126	syl5ibcom 244	. . . . . 6 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
128	127	rexlimdvva 3209	. . . . 5 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
129	6, 128	biimtrrid 242	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
130	5, 129	sylbid 239	. . 3 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
131	130	ralrimivv 3196	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))
132		df-so 5595	. 2 ⊢ (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
133	1, 131, 132	sylanbrc 581	1 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∀wral 3058  ∃wrex 3067   ⊆ wss 3949   class class class wbr 5152   Po wpo 5592   Or wor 5593  ran crn 5683  Ord word 6373  suc csuc 6376   Fn wfn 6548  ‘cfv 6553  ωcom 7876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-fv 6561  df-om 7877

This theorem is referenced by:  fin23lem40  10382