MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sornom Structured version   Visualization version   GIF version

Theorem sornom 8858
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.
StepHypRef Expression
1 simp3 1055 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2 fvelrnb 6037 . . . . . 6 (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹𝑑) = 𝑏))
3 fvelrnb 6037 . . . . . 6 (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
42, 3anbi12d 742 . . . . 5 (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
543ad2ant1 1074 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
6 reeanv 2990 . . . . 5 (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
7 nnord 6841 . . . . . . . . . . 11 (𝑑 ∈ ω → Ord 𝑑)
8 nnord 6841 . . . . . . . . . . 11 (𝑒 ∈ ω → Ord 𝑒)
9 ordtri2or2 5626 . . . . . . . . . . 11 ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑𝑒𝑒𝑑))
107, 8, 9syl2an 492 . . . . . . . . . 10 ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑𝑒𝑒𝑑))
1110adantl 480 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒𝑒𝑑))
12 vex 3080 . . . . . . . . . . 11 𝑑 ∈ V
13 vex 3080 . . . . . . . . . . 11 𝑒 ∈ V
14 eleq1 2580 . . . . . . . . . . . . . 14 (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15 eleq1 2580 . . . . . . . . . . . . . 14 (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
1614, 15bi2anan9 912 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
1716anbi2d 735 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18 sseq12 3495 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (𝑏𝑐𝑑𝑒))
19 fveq2 5987 . . . . . . . . . . . . . . 15 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
20 fveq2 5987 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 → (𝐹𝑐) = (𝐹𝑒))
2119, 20breqan12d 4497 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑑)𝑅(𝐹𝑒)))
2219, 20eqeqan12d 2530 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑑) = (𝐹𝑒)))
2321, 22orbi12d 741 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
2418, 23imbi12d 332 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)))))
2517, 24imbi12d 332 . . . . . . . . . . 11 ((𝑏 = 𝑑𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))))
26 fveq2 5987 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝐹𝑑) = (𝐹𝑏))
2726breq2d 4493 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑏)))
2826eqeq2d 2524 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑏)))
2927, 28orbi12d 741 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
3029imbi2d 328 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏)))))
31 fveq2 5987 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑒 → (𝐹𝑑) = (𝐹𝑒))
3231breq2d 4493 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑒)))
3331eqeq2d 2524 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑒)))
3432, 33orbi12d 741 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒))))
3534imbi2d 328 . . . . . . . . . . . . . . 15 (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)))))
36 fveq2 5987 . . . . . . . . . . . . . . . . . 18 (𝑑 = suc 𝑒 → (𝐹𝑑) = (𝐹‘suc 𝑒))
3736breq2d 4493 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
3836eqeq2d 2524 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
3937, 38orbi12d 741 . . . . . . . . . . . . . . . 16 (𝑑 = suc 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
4039imbi2d 328 . . . . . . . . . . . . . . 15 (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
41 fveq2 5987 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
4241breq2d 4493 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑐)))
4341eqeq2d 2524 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑐)))
4442, 43orbi12d 741 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑐 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
4544imbi2d 328 . . . . . . . . . . . . . . 15 (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))))
46 eqid 2514 . . . . . . . . . . . . . . . . 17 (𝐹𝑏) = (𝐹𝑏)
4746olci 404 . . . . . . . . . . . . . . . 16 ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))
48472a1i 12 . . . . . . . . . . . . . . 15 (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
49 simplll 793 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
50 simpr2 1060 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)))
51 fveq2 5987 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
52 suceq 5595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
5352fveq2d 5991 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
5451, 53breq12d 4494 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
5551, 53eqeq12d 2529 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → ((𝐹𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹𝑒) = (𝐹‘suc 𝑒)))
5654, 55orbi12d 741 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑒 → (((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒))))
5756rspcva 3184 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎))) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)))
5849, 50, 57syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)))
59 simprr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
60 simprl 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
61 simpllr 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
62 fnfvelrn 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹𝑏) ∈ ran 𝐹)
6360, 61, 62syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑏) ∈ ran 𝐹)
64 simplll 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
65 fnfvelrn 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹𝑒) ∈ ran 𝐹)
6660, 64, 65syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑒) ∈ ran 𝐹)
67 peano2 6854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 ∈ ω → suc 𝑒 ∈ ω)
6867ad3antrrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
69 fnfvelrn 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
7060, 68, 69syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
71 potr 4865 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po ran 𝐹 ∧ ((𝐹𝑏) ∈ ran 𝐹 ∧ (𝐹𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7259, 63, 66, 70, 71syl13anc 1319 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7372imp 443 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7473ancom2s 839 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7574orcd 405 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
7675expr 640 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏)𝑅(𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
77 breq1 4484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
7877biimprcd 238 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
79 orc 398 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
8078, 79syl6 34 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8180adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8276, 81jaod 393 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8382ex 448 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
84 breq2 4485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑒) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
85 eqeq2 2525 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
8684, 85orbi12d 741 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8786biimpd 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8887a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
8983, 88jaod 393 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
90893adantr2 1213 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9158, 90mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
9291ex 448 . . . . . . . . . . . . . . . 16 (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9392a2d 29 . . . . . . . . . . . . . . 15 (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒))) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9430, 35, 40, 45, 48, 93findsg 6861 . . . . . . . . . . . . . 14 (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9594ancom1s 842 . . . . . . . . . . . . 13 (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9695impcom 444 . . . . . . . . . . . 12 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐)) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))
9796expr 640 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9812, 13, 25, 97vtocl2 3138 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
99 eleq1 2580 . . . . . . . . . . . . . . 15 (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
100 eleq1 2580 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
10199, 100bi2anan9 912 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
102101anbi2d 735 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
103 sseq12 3495 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (𝑏𝑐𝑒𝑑))
104 fveq2 5987 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 → (𝐹𝑏) = (𝐹𝑒))
105 fveq2 5987 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (𝐹𝑐) = (𝐹𝑑))
106104, 105breqan12d 4497 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑒)𝑅(𝐹𝑑)))
107104, 105eqeqan12d 2530 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑒) = (𝐹𝑑)))
108106, 107orbi12d 741 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
109103, 108imbi12d 332 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
110102, 109imbi12d 332 . . . . . . . . . . . 12 ((𝑏 = 𝑒𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))))
11113, 12, 110, 97vtocl2 3138 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
112111ancom2s 839 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
11398, 112orim12d 878 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑𝑒𝑒𝑑) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
11411, 113mpd 15 . . . . . . . 8 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
115 3mix1 1222 . . . . . . . . . 10 ((𝐹𝑑)𝑅(𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
116 3mix2 1223 . . . . . . . . . 10 ((𝐹𝑑) = (𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
117115, 116jaoi 392 . . . . . . . . 9 (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
118 3mix3 1224 . . . . . . . . . 10 ((𝐹𝑒)𝑅(𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
119116eqcoms 2522 . . . . . . . . . 10 ((𝐹𝑒) = (𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
120118, 119jaoi 392 . . . . . . . . 9 (((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
121117, 120jaoi 392 . . . . . . . 8 ((((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
122114, 121syl 17 . . . . . . 7 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
123 breq12 4486 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑)𝑅(𝐹𝑒) ↔ 𝑏𝑅𝑐))
124 eqeq12 2527 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑) = (𝐹𝑒) ↔ 𝑏 = 𝑐))
125 breq12 4486 . . . . . . . . 9 (((𝐹𝑒) = 𝑐 ∧ (𝐹𝑑) = 𝑏) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
126125ancoms 467 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
127123, 124, 1263orbi123d 1389 . . . . . . 7 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)) ↔ (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
128122, 127syl5ibcom 233 . . . . . 6 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
129128rexlimdvva 2924 . . . . 5 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1306, 129syl5bir 231 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1315, 130sylbid 228 . . 3 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
132131ralrimivv 2857 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏))
133 df-so 4854 . 2 (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1341, 132, 133sylanbrc 694 1 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3o 1029  w3a 1030   = wceq 1474  wcel 1938  wral 2800  wrex 2801  wss 3444   class class class wbr 4481   Po wpo 4851   Or wor 4852  ran crn 4933  Ord word 5529  suc csuc 5532   Fn wfn 5684  cfv 5689  ωcom 6833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732  ax-un 6723
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-fv 5697  df-om 6834
This theorem is referenced by:  fin23lem40  8932
  Copyright terms: Public domain W3C validator