Theorem sornom 10171

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 1138	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2		fvelrnb 6883	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏))
3		fvelrnb 6883	. . . . . 6 ⊢ (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
4	2, 3	anbi12d 632	. . . . 5 ⊢ (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
5	4	3ad2ant1 1133	. . . 4 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)))
6		reeanv 3201	. . . . 5 ⊢ (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))
7		nnord 7807	. . . . . . . . . . 11 ⊢ (𝑑 ∈ ω → Ord 𝑑)
8		nnord 7807	. . . . . . . . . . 11 ⊢ (𝑒 ∈ ω → Ord 𝑒)
9		ordtri2or2 6408	. . . . . . . . . . 11 ⊢ ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
10	7, 8, 9	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
11	10	adantl 481	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑))
12		vex 3440	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
13		vex 3440	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
14		eleq1w 2811	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15		eleq1w 2811	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
16	14, 15	bi2anan9 638	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
17	16	anbi2d 630	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18		sseq12 3963	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (𝑏 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑒))
19		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
20		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → (𝐹‘𝑐) = (𝐹‘𝑒))
21	19, 20	breqan12d 5108	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑒)))
22	19, 20	eqeqan12d 2743	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑑) = (𝐹‘𝑒)))
23	21, 22	orbi12d 918	. . . . . . . . . . . . 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 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝐹‘𝑑) = (𝐹‘𝑏))
27	26	breq2d 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑏)))
28	26	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑏)))
29	27, 28	orbi12d 918	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
30	29	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)))))
31		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑒 → (𝐹‘𝑑) = (𝐹‘𝑒))
32	31	breq2d 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑒)))
33	31	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑒)))
34	32, 33	orbi12d 918	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))))
35	34	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)))))
36		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = suc 𝑒 → (𝐹‘𝑑) = (𝐹‘suc 𝑒))
37	36	breq2d 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
38	36	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
39	37, 38	orbi12d 918	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = suc 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
40	39	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
41		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
42	41	breq2d 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑐)))
43	41	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑐)))
44	42, 43	orbi12d 918	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
45	44	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))))
46		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑏) = (𝐹‘𝑏)
47	46	olci 866	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))
48	47	2a1i 12	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))
49		fveq2 6822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘𝑎) = (𝐹‘𝑒))
50		suceq 6375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
51	50	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
52	49, 51	breq12d 5105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
53	49, 51	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
54	52, 53	orbi12d 918	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑒 → (((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒))))
55		simpr2 1196	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)))
56		simplll 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
57	54, 55, 56	rspcdva 3578	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))
58		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
59		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
60		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
61		fnfvelrn 7014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹‘𝑏) ∈ ran 𝐹)
62	59, 60, 61	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑏) ∈ ran 𝐹)
63		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
64		fnfvelrn 7014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹‘𝑒) ∈ ran 𝐹)
65	59, 63, 64	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑒) ∈ ran 𝐹)
66		peano2 7823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 ∈ ω → suc 𝑒 ∈ ω)
67	66	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
68		fnfvelrn 7014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
69	59, 67, 68	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
70		potr 5540	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po ran 𝐹 ∧ ((𝐹‘𝑏) ∈ ran 𝐹 ∧ (𝐹‘𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
71	58, 62, 65, 69, 70	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
72	71	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
73	72	ancom2s 650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))
74	73	orcd 873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
75	74	expr 456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
76		breq1 5095	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)))
77	76	biimprcd 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
78		orc 867	. . . . . . . . . . . . . . . . . . . . . . . 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 859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))
82	81	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
83		breq2 5096	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)))
84		eqeq2 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))
85	83, 84	orbi12d 918	. . . . . . . . . . . . . . . . . . . . . 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 859	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))))
89	88	3adantr2 1171	. . . . . . . . . . . . . . . . . 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 7830	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))
94	93	ancom1s 653	. . . . . . . . . . . . 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 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
99		eleq1w 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
100	98, 99	bi2anan9 638	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
101	100	anbi2d 630	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
102		sseq12 3963	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (𝑏 ⊆ 𝑐 ↔ 𝑒 ⊆ 𝑑))
103		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝐹‘𝑏) = (𝐹‘𝑒))
104		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑑 → (𝐹‘𝑐) = (𝐹‘𝑑))
105	103, 104	breqan12d 5108	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
106	103, 104	eqeqan12d 2743	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑒) = (𝐹‘𝑑)))
107	105, 106	orbi12d 918	. . . . . . . . . . . . . 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 650	. . . . . . . . . 10 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
112	97, 111	orim12d 966	. . . . . . . . 9 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))
113	11, 112	mpd 15	. . . . . . . 8 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))
114		3mix1 1331	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
115		3mix2 1332	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑) = (𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
116	114, 115	jaoi 857	. . . . . . . . 9 ⊢ (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
117		3mix3 1333	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
118	115	eqcoms 2737	. . . . . . . . . 10 ⊢ ((𝐹‘𝑒) = (𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
119	117, 118	jaoi 857	. . . . . . . . 9 ⊢ (((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
120	116, 119	jaoi 857	. . . . . . . 8 ⊢ ((((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
121	113, 120	syl 17	. . . . . . 7 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)))
122		breq12 5097	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ↔ 𝑏𝑅𝑐))
123		eqeq12 2746	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑) = (𝐹‘𝑒) ↔ 𝑏 = 𝑐))
124		breq12 5097	. . . . . . . . 9 ⊢ (((𝐹‘𝑒) = 𝑐 ∧ (𝐹‘𝑑) = 𝑏) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
125	124	ancoms 458	. . . . . . . 8 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏))
126	122, 123, 125	3orbi123d 1437	. . . . . . 7 ⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)) ↔ (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
127	121, 126	syl5ibcom 245	. . . . . 6 ⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
128	127	rexlimdvva 3186	. . . . 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 3170	. 2 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))
132		df-so 5528	. 2 ⊢ (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)))
133	1, 131, 132	sylanbrc 583	1 ⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   ⊆ wss 3903   class class class wbr 5092   Po wpo 5525   Or wor 5526  ran crn 5620  Ord word 6306  suc csuc 6309   Fn wfn 6477  ‘cfv 6482  ωcom 7799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490  df-om 7800

This theorem is referenced by:  fin23lem40  10245