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

Theorem sornom 8982
 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 1056 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2 fvelrnb 6153 . . . . . 6 (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹𝑑) = 𝑏))
3 fvelrnb 6153 . . . . . 6 (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
42, 3anbi12d 743 . . . . 5 (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
543ad2ant1 1075 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
6 reeanv 3086 . . . . 5 (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
7 nnord 6965 . . . . . . . . . . 11 (𝑑 ∈ ω → Ord 𝑑)
8 nnord 6965 . . . . . . . . . . 11 (𝑒 ∈ ω → Ord 𝑒)
9 ordtri2or2 5740 . . . . . . . . . . 11 ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑𝑒𝑒𝑑))
107, 8, 9syl2an 493 . . . . . . . . . 10 ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑𝑒𝑒𝑑))
1110adantl 481 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒𝑒𝑑))
12 vex 3176 . . . . . . . . . . 11 𝑑 ∈ V
13 vex 3176 . . . . . . . . . . 11 𝑒 ∈ V
14 eleq1 2676 . . . . . . . . . . . . . 14 (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15 eleq1 2676 . . . . . . . . . . . . . 14 (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
1614, 15bi2anan9 913 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
1716anbi2d 736 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18 sseq12 3591 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (𝑏𝑐𝑑𝑒))
19 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
20 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 → (𝐹𝑐) = (𝐹𝑒))
2119, 20breqan12d 4599 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑑)𝑅(𝐹𝑒)))
2219, 20eqeqan12d 2626 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑑) = (𝐹𝑒)))
2321, 22orbi12d 742 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
2418, 23imbi12d 333 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)))))
2517, 24imbi12d 333 . . . . . . . . . . 11 ((𝑏 = 𝑑𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))))
26 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝐹𝑑) = (𝐹𝑏))
2726breq2d 4595 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑏)))
2826eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑏)))
2927, 28orbi12d 742 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
3029imbi2d 329 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏)))))
31 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑒 → (𝐹𝑑) = (𝐹𝑒))
3231breq2d 4595 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑒)))
3331eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑒)))
3432, 33orbi12d 742 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒))))
3534imbi2d 329 . . . . . . . . . . . . . . 15 (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)))))
36 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑑 = suc 𝑒 → (𝐹𝑑) = (𝐹‘suc 𝑒))
3736breq2d 4595 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
3836eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
3937, 38orbi12d 742 . . . . . . . . . . . . . . . 16 (𝑑 = suc 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
4039imbi2d 329 . . . . . . . . . . . . . . 15 (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
41 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
4241breq2d 4595 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑐)))
4341eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑐)))
4442, 43orbi12d 742 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑐 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
4544imbi2d 329 . . . . . . . . . . . . . . 15 (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))))
46 eqid 2610 . . . . . . . . . . . . . . . . 17 (𝐹𝑏) = (𝐹𝑏)
4746olci 405 . . . . . . . . . . . . . . . 16 ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))
48472a1i 12 . . . . . . . . . . . . . . 15 (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
49 simplll 794 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
50 simpr2 1061 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)))
51 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
52 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
5352fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
5451, 53breq12d 4596 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
5551, 53eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → ((𝐹𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹𝑒) = (𝐹‘suc 𝑒)))
5654, 55orbi12d 742 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑒 → (((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒))))
5756rspcva 3280 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎))) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)))
5849, 50, 57syl2anc 691 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)))
59 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
60 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
61 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
62 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹𝑏) ∈ ran 𝐹)
6360, 61, 62syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑏) ∈ ran 𝐹)
64 simplll 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
65 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹𝑒) ∈ ran 𝐹)
6660, 64, 65syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑒) ∈ ran 𝐹)
67 peano2 6978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 ∈ ω → suc 𝑒 ∈ ω)
6867ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
69 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
7060, 68, 69syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
71 potr 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po ran 𝐹 ∧ ((𝐹𝑏) ∈ ran 𝐹 ∧ (𝐹𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7259, 63, 66, 70, 71syl13anc 1320 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7372imp 444 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7473ancom2s 840 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7574orcd 406 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
7675expr 641 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏)𝑅(𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
77 breq1 4586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
7877biimprcd 239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
79 orc 399 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
8078, 79syl6 34 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8180adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8276, 81jaod 394 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8382ex 449 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
84 breq2 4587 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑒) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
85 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
8684, 85orbi12d 742 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8786biimpd 218 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8887a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
8983, 88jaod 394 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
90893adantr2 1214 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9158, 90mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
9291ex 449 . . . . . . . . . . . . . . . 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 6985 . . . . . . . . . . . . . 14 (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9594ancom1s 843 . . . . . . . . . . . . 13 (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9695impcom 445 . . . . . . . . . . . 12 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐)) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))
9796expr 641 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9812, 13, 25, 97vtocl2 3234 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
99 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
100 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
10199, 100bi2anan9 913 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
102101anbi2d 736 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
103 sseq12 3591 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (𝑏𝑐𝑒𝑑))
104 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 → (𝐹𝑏) = (𝐹𝑒))
105 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (𝐹𝑐) = (𝐹𝑑))
106104, 105breqan12d 4599 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑒)𝑅(𝐹𝑑)))
107104, 105eqeqan12d 2626 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑒) = (𝐹𝑑)))
108106, 107orbi12d 742 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
109103, 108imbi12d 333 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
110102, 109imbi12d 333 . . . . . . . . . . . 12 ((𝑏 = 𝑒𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))))
11113, 12, 110, 97vtocl2 3234 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
112111ancom2s 840 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
11398, 112orim12d 879 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑𝑒𝑒𝑑) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
11411, 113mpd 15 . . . . . . . 8 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
115 3mix1 1223 . . . . . . . . . 10 ((𝐹𝑑)𝑅(𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
116 3mix2 1224 . . . . . . . . . 10 ((𝐹𝑑) = (𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
117115, 116jaoi 393 . . . . . . . . 9 (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
118 3mix3 1225 . . . . . . . . . 10 ((𝐹𝑒)𝑅(𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
119116eqcoms 2618 . . . . . . . . . 10 ((𝐹𝑒) = (𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
120118, 119jaoi 393 . . . . . . . . 9 (((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
121117, 120jaoi 393 . . . . . . . 8 ((((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
122114, 121syl 17 . . . . . . 7 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
123 breq12 4588 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑)𝑅(𝐹𝑒) ↔ 𝑏𝑅𝑐))
124 eqeq12 2623 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑) = (𝐹𝑒) ↔ 𝑏 = 𝑐))
125 breq12 4588 . . . . . . . . 9 (((𝐹𝑒) = 𝑐 ∧ (𝐹𝑑) = 𝑏) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
126125ancoms 468 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
127123, 124, 1263orbi123d 1390 . . . . . . 7 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)) ↔ (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
128122, 127syl5ibcom 234 . . . . . 6 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
129128rexlimdvva 3020 . . . . 5 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1306, 129syl5bir 232 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1315, 130sylbid 229 . . 3 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
132131ralrimivv 2953 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏))
133 df-so 4960 . 2 (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1341, 132, 133sylanbrc 695 1 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540   class class class wbr 4583   Po wpo 4957   Or wor 4958  ran crn 5039  Ord word 5639  suc csuc 5642   Fn wfn 5799  ‘cfv 5804  ωcom 6957 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-om 6958 This theorem is referenced by:  fin23lem40  9056
 Copyright terms: Public domain W3C validator