This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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