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

Theorem sornom 10276
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 1136 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2 fvelrnb 6953 . . . . . 6 (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹𝑑) = 𝑏))
3 fvelrnb 6953 . . . . . 6 (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
42, 3anbi12d 629 . . . . 5 (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
543ad2ant1 1131 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
6 reeanv 3224 . . . . 5 (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
7 nnord 7867 . . . . . . . . . . 11 (𝑑 ∈ ω → Ord 𝑑)
8 nnord 7867 . . . . . . . . . . 11 (𝑒 ∈ ω → Ord 𝑒)
9 ordtri2or2 6464 . . . . . . . . . . 11 ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑𝑒𝑒𝑑))
107, 8, 9syl2an 594 . . . . . . . . . 10 ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑𝑒𝑒𝑑))
1110adantl 480 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒𝑒𝑑))
12 vex 3476 . . . . . . . . . . 11 𝑑 ∈ V
13 vex 3476 . . . . . . . . . . 11 𝑒 ∈ V
14 eleq1w 2814 . . . . . . . . . . . . . 14 (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15 eleq1w 2814 . . . . . . . . . . . . . 14 (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
1614, 15bi2anan9 635 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
1716anbi2d 627 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18 sseq12 4010 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (𝑏𝑐𝑑𝑒))
19 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
20 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 → (𝐹𝑐) = (𝐹𝑒))
2119, 20breqan12d 5165 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑑)𝑅(𝐹𝑒)))
2219, 20eqeqan12d 2744 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑑) = (𝐹𝑒)))
2321, 22orbi12d 915 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
2418, 23imbi12d 343 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)))))
2517, 24imbi12d 343 . . . . . . . . . . 11 ((𝑏 = 𝑑𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))))
26 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝐹𝑑) = (𝐹𝑏))
2726breq2d 5161 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑏)))
2826eqeq2d 2741 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑏)))
2927, 28orbi12d 915 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
3029imbi2d 339 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏)))))
31 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑒 → (𝐹𝑑) = (𝐹𝑒))
3231breq2d 5161 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑒)))
3331eqeq2d 2741 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑒)))
3432, 33orbi12d 915 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒))))
3534imbi2d 339 . . . . . . . . . . . . . . 15 (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)))))
36 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (𝑑 = suc 𝑒 → (𝐹𝑑) = (𝐹‘suc 𝑒))
3736breq2d 5161 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
3836eqeq2d 2741 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
3937, 38orbi12d 915 . . . . . . . . . . . . . . . 16 (𝑑 = suc 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
4039imbi2d 339 . . . . . . . . . . . . . . 15 (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
41 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
4241breq2d 5161 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑐)))
4341eqeq2d 2741 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑐)))
4442, 43orbi12d 915 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑐 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
4544imbi2d 339 . . . . . . . . . . . . . . 15 (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))))
46 eqid 2730 . . . . . . . . . . . . . . . . 17 (𝐹𝑏) = (𝐹𝑏)
4746olci 862 . . . . . . . . . . . . . . . 16 ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))
48472a1i 12 . . . . . . . . . . . . . . 15 (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
49 fveq2 6892 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
50 suceq 6431 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
5150fveq2d 6896 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
5249, 51breq12d 5162 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑒 → ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
5349, 51eqeq12d 2746 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑒 → ((𝐹𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹𝑒) = (𝐹‘suc 𝑒)))
5452, 53orbi12d 915 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑒 → (((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒))))
55 simpr2 1193 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)))
56 simplll 771 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
5754, 55, 56rspcdva 3614 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)))
58 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
59 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
60 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
61 fnfvelrn 7083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹𝑏) ∈ ran 𝐹)
6259, 60, 61syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑏) ∈ ran 𝐹)
63 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
64 fnfvelrn 7083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹𝑒) ∈ ran 𝐹)
6559, 63, 64syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑒) ∈ ran 𝐹)
66 peano2 7885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 ∈ ω → suc 𝑒 ∈ ω)
6766ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
68 fnfvelrn 7083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
6959, 67, 68syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
70 potr 5602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po ran 𝐹 ∧ ((𝐹𝑏) ∈ ran 𝐹 ∧ (𝐹𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7158, 62, 65, 69, 70syl13anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7271imp 405 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7372ancom2s 646 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7473orcd 869 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
7574expr 455 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏)𝑅(𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
76 breq1 5152 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
7776biimprcd 249 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
78 orc 863 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
7977, 78syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8079adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8175, 80jaod 855 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8281ex 411 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
83 breq2 5153 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑒) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
84 eqeq2 2742 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
8583, 84orbi12d 915 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8685biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8786a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
8882, 87jaod 855 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
89883adantr2 1168 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9057, 89mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
9190ex 411 . . . . . . . . . . . . . . . 16 (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9291a2d 29 . . . . . . . . . . . . . . 15 (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒))) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9330, 35, 40, 45, 48, 92findsg 7894 . . . . . . . . . . . . . 14 (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9493ancom1s 649 . . . . . . . . . . . . 13 (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9594impcom 406 . . . . . . . . . . . 12 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐)) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))
9695expr 455 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9712, 13, 25, 96vtocl2 3553 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
98 eleq1w 2814 . . . . . . . . . . . . . . 15 (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
99 eleq1w 2814 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
10098, 99bi2anan9 635 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
101100anbi2d 627 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
102 sseq12 4010 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (𝑏𝑐𝑒𝑑))
103 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 → (𝐹𝑏) = (𝐹𝑒))
104 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (𝐹𝑐) = (𝐹𝑑))
105103, 104breqan12d 5165 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑒)𝑅(𝐹𝑑)))
106103, 104eqeqan12d 2744 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑒) = (𝐹𝑑)))
107105, 106orbi12d 915 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
108102, 107imbi12d 343 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
109101, 108imbi12d 343 . . . . . . . . . . . 12 ((𝑏 = 𝑒𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))))
11013, 12, 109, 96vtocl2 3553 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
111110ancom2s 646 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
11297, 111orim12d 961 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑𝑒𝑒𝑑) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
11311, 112mpd 15 . . . . . . . 8 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
114 3mix1 1328 . . . . . . . . . 10 ((𝐹𝑑)𝑅(𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
115 3mix2 1329 . . . . . . . . . 10 ((𝐹𝑑) = (𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
116114, 115jaoi 853 . . . . . . . . 9 (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
117 3mix3 1330 . . . . . . . . . 10 ((𝐹𝑒)𝑅(𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
118115eqcoms 2738 . . . . . . . . . 10 ((𝐹𝑒) = (𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
119117, 118jaoi 853 . . . . . . . . 9 (((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
120116, 119jaoi 853 . . . . . . . 8 ((((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
121113, 120syl 17 . . . . . . 7 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
122 breq12 5154 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑)𝑅(𝐹𝑒) ↔ 𝑏𝑅𝑐))
123 eqeq12 2747 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑) = (𝐹𝑒) ↔ 𝑏 = 𝑐))
124 breq12 5154 . . . . . . . . 9 (((𝐹𝑒) = 𝑐 ∧ (𝐹𝑑) = 𝑏) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
125124ancoms 457 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
126122, 123, 1253orbi123d 1433 . . . . . . 7 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)) ↔ (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
127121, 126syl5ibcom 244 . . . . . 6 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
128127rexlimdvva 3209 . . . . 5 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1296, 128biimtrrid 242 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1305, 129sylbid 239 . . 3 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
131130ralrimivv 3196 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏))
132 df-so 5590 . 2 (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1331, 131, 132sylanbrc 581 1 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 843  w3o 1084  w3a 1085   = wceq 1539  wcel 2104  wral 3059  wrex 3068  wss 3949   class class class wbr 5149   Po wpo 5587   Or wor 5588  ran crn 5678  Ord word 6364  suc csuc 6367   Fn wfn 6539  cfv 6544  ωcom 7859
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552  df-om 7860
This theorem is referenced by:  fin23lem40  10350
  Copyright terms: Public domain W3C validator