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

Theorem sornom 10213
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 1138 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹)
2 fvelrnb 6903 . . . . . 6 (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹𝑑) = 𝑏))
3 fvelrnb 6903 . . . . . 6 (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
42, 3anbi12d 631 . . . . 5 (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
543ad2ant1 1133 . . . 4 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐)))
6 reeanv 3217 . . . . 5 (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹𝑒) = 𝑐))
7 nnord 7810 . . . . . . . . . . 11 (𝑑 ∈ ω → Ord 𝑑)
8 nnord 7810 . . . . . . . . . . 11 (𝑒 ∈ ω → Ord 𝑒)
9 ordtri2or2 6416 . . . . . . . . . . 11 ((Ord 𝑑 ∧ Ord 𝑒) → (𝑑𝑒𝑒𝑑))
107, 8, 9syl2an 596 . . . . . . . . . 10 ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑𝑒𝑒𝑑))
1110adantl 482 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒𝑒𝑑))
12 vex 3449 . . . . . . . . . . 11 𝑑 ∈ V
13 vex 3449 . . . . . . . . . . 11 𝑒 ∈ V
14 eleq1w 2820 . . . . . . . . . . . . . 14 (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω))
15 eleq1w 2820 . . . . . . . . . . . . . 14 (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω))
1614, 15bi2anan9 637 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))
1716anbi2d 629 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))))
18 sseq12 3971 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (𝑏𝑐𝑑𝑒))
19 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
20 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 → (𝐹𝑐) = (𝐹𝑒))
2119, 20breqan12d 5121 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑑)𝑅(𝐹𝑒)))
2219, 20eqeqan12d 2750 . . . . . . . . . . . . . 14 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑑) = (𝐹𝑒)))
2321, 22orbi12d 917 . . . . . . . . . . . . 13 ((𝑏 = 𝑑𝑐 = 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
2418, 23imbi12d 344 . . . . . . . . . . . 12 ((𝑏 = 𝑑𝑐 = 𝑒) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)))))
2517, 24imbi12d 344 . . . . . . . . . . 11 ((𝑏 = 𝑑𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))))
26 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝐹𝑑) = (𝐹𝑏))
2726breq2d 5117 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑏)))
2826eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑏)))
2927, 28orbi12d 917 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
3029imbi2d 340 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏)))))
31 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑒 → (𝐹𝑑) = (𝐹𝑒))
3231breq2d 5117 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑒)))
3331eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑒)))
3432, 33orbi12d 917 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒))))
3534imbi2d 340 . . . . . . . . . . . . . . 15 (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)))))
36 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑑 = suc 𝑒 → (𝐹𝑑) = (𝐹‘suc 𝑒))
3736breq2d 5117 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
3836eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑑 = suc 𝑒 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
3937, 38orbi12d 917 . . . . . . . . . . . . . . . 16 (𝑑 = suc 𝑒 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
4039imbi2d 340 . . . . . . . . . . . . . . 15 (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
41 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
4241breq2d 5117 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏)𝑅(𝐹𝑑) ↔ (𝐹𝑏)𝑅(𝐹𝑐)))
4341eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑏) = (𝐹𝑐)))
4442, 43orbi12d 917 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑐 → (((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑)) ↔ ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
4544imbi2d 340 . . . . . . . . . . . . . . 15 (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑑) ∨ (𝐹𝑏) = (𝐹𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))))
46 eqid 2736 . . . . . . . . . . . . . . . . 17 (𝐹𝑏) = (𝐹𝑏)
4746olci 864 . . . . . . . . . . . . . . . 16 ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))
48472a1i 12 . . . . . . . . . . . . . . 15 (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑏) ∨ (𝐹𝑏) = (𝐹𝑏))))
49 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
50 suceq 6383 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒)
5150fveq2d 6846 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒))
5249, 51breq12d 5118 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑒 → ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
5349, 51eqeq12d 2752 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑒 → ((𝐹𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹𝑒) = (𝐹‘suc 𝑒)))
5452, 53orbi12d 917 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑒 → (((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒))))
55 simpr2 1195 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)))
56 simplll 773 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
5754, 55, 56rspcdva 3582 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)))
58 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹)
59 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω)
60 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω)
61 fnfvelrn 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹𝑏) ∈ ran 𝐹)
6259, 60, 61syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑏) ∈ ran 𝐹)
63 simplll 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω)
64 fnfvelrn 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹𝑒) ∈ ran 𝐹)
6559, 63, 64syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹𝑒) ∈ ran 𝐹)
66 peano2 7827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 ∈ ω → suc 𝑒 ∈ ω)
6766ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω)
68 fnfvelrn 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
6959, 67, 68syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹)
70 potr 5558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po ran 𝐹 ∧ ((𝐹𝑏) ∈ ran 𝐹 ∧ (𝐹𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7158, 62, 65, 69, 70syl13anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
7271imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑏)𝑅(𝐹𝑒) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7372ancom2s 648 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒))
7473orcd 871 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹𝑏)𝑅(𝐹𝑒))) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
7574expr 457 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏)𝑅(𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
76 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)))
7776biimprcd 249 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
78 orc 865 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))
7977, 78syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8079adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹𝑏) = (𝐹𝑒) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8175, 80jaod 857 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8281ex 413 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
83 breq2 5109 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏)𝑅(𝐹𝑒) ↔ (𝐹𝑏)𝑅(𝐹‘suc 𝑒)))
84 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑒) = (𝐹‘suc 𝑒) → ((𝐹𝑏) = (𝐹𝑒) ↔ (𝐹𝑏) = (𝐹‘suc 𝑒)))
8583, 84orbi12d 917 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) ↔ ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8685biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
8786a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹𝑒) = (𝐹‘suc 𝑒) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
8882, 87jaod 857 . . . . . . . . . . . . . . . . . . 19 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
89883adantr2 1170 . . . . . . . . . . . . . . . . . 18 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑒) = (𝐹‘suc 𝑒)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒)))))
9057, 89mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹𝑏)𝑅(𝐹𝑒) ∨ (𝐹𝑏) = (𝐹𝑒)) → ((𝐹𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹𝑏) = (𝐹‘suc 𝑒))))
9190ex 413 . . . . . . . . . . . . . . . 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 7836 . . . . . . . . . . . . . 14 (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9493ancom1s 651 . . . . . . . . . . . . 13 (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9594impcom 408 . . . . . . . . . . . 12 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏𝑐)) → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))
9695expr 457 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))))
9712, 13, 25, 96vtocl2 3520 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑𝑒 → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒))))
98 eleq1w 2820 . . . . . . . . . . . . . . 15 (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω))
99 eleq1w 2820 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω))
10098, 99bi2anan9 637 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))
101100anbi2d 629 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))))
102 sseq12 3971 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (𝑏𝑐𝑒𝑑))
103 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 → (𝐹𝑏) = (𝐹𝑒))
104 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (𝐹𝑐) = (𝐹𝑑))
105103, 104breqan12d 5121 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏)𝑅(𝐹𝑐) ↔ (𝐹𝑒)𝑅(𝐹𝑑)))
106103, 104eqeqan12d 2750 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝐹𝑏) = (𝐹𝑐) ↔ (𝐹𝑒) = (𝐹𝑑)))
107105, 106orbi12d 917 . . . . . . . . . . . . . 14 ((𝑏 = 𝑒𝑐 = 𝑑) → (((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)) ↔ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
108102, 107imbi12d 344 . . . . . . . . . . . . 13 ((𝑏 = 𝑒𝑐 = 𝑑) → ((𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐))) ↔ (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
109101, 108imbi12d 344 . . . . . . . . . . . 12 ((𝑏 = 𝑒𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏𝑐 → ((𝐹𝑏)𝑅(𝐹𝑐) ∨ (𝐹𝑏) = (𝐹𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))))
11013, 12, 109, 96vtocl2 3520 . . . . . . . . . . 11 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
111110ancom2s 648 . . . . . . . . . 10 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒𝑑 → ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
11297, 111orim12d 963 . . . . . . . . 9 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑𝑒𝑒𝑑) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)))))
11311, 112mpd 15 . . . . . . . 8 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))))
114 3mix1 1330 . . . . . . . . . 10 ((𝐹𝑑)𝑅(𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
115 3mix2 1331 . . . . . . . . . 10 ((𝐹𝑑) = (𝐹𝑒) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
116114, 115jaoi 855 . . . . . . . . 9 (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
117 3mix3 1332 . . . . . . . . . 10 ((𝐹𝑒)𝑅(𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
118115eqcoms 2744 . . . . . . . . . 10 ((𝐹𝑒) = (𝐹𝑑) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
119117, 118jaoi 855 . . . . . . . . 9 (((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
120116, 119jaoi 855 . . . . . . . 8 ((((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒)) ∨ ((𝐹𝑒)𝑅(𝐹𝑑) ∨ (𝐹𝑒) = (𝐹𝑑))) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
121113, 120syl 17 . . . . . . 7 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)))
122 breq12 5110 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑)𝑅(𝐹𝑒) ↔ 𝑏𝑅𝑐))
123 eqeq12 2753 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑑) = (𝐹𝑒) ↔ 𝑏 = 𝑐))
124 breq12 5110 . . . . . . . . 9 (((𝐹𝑒) = 𝑐 ∧ (𝐹𝑑) = 𝑏) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
125124ancoms 459 . . . . . . . 8 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → ((𝐹𝑒)𝑅(𝐹𝑑) ↔ 𝑐𝑅𝑏))
126122, 123, 1253orbi123d 1435 . . . . . . 7 (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (((𝐹𝑑)𝑅(𝐹𝑒) ∨ (𝐹𝑑) = (𝐹𝑒) ∨ (𝐹𝑒)𝑅(𝐹𝑑)) ↔ (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
127121, 126syl5ibcom 244 . . . . . 6 (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹𝑑) = 𝑏 ∧ (𝐹𝑒) = 𝑐) → (𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
128127rexlimdvva 3205 . . . . 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 3195 . 2 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏))
132 df-so 5546 . 2 (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹𝑐 ∈ ran 𝐹(𝑏𝑅𝑐𝑏 = 𝑐𝑐𝑅𝑏)))
1331, 131, 132sylanbrc 583 1 ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  wss 3910   class class class wbr 5105   Po wpo 5543   Or wor 5544  ran crn 5634  Ord word 6316  suc csuc 6319   Fn wfn 6491  cfv 6496  ωcom 7802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-fv 6504  df-om 7803
This theorem is referenced by:  fin23lem40  10287
  Copyright terms: Public domain W3C validator