| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp3 1138 | . 2
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Po ran 𝐹) | 
| 2 |  | fvelrnb 6968 | . . . . . 6
⊢ (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏)) | 
| 3 |  | fvelrnb 6968 | . . . . . 6
⊢ (𝐹 Fn ω → (𝑐 ∈ ran 𝐹 ↔ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)) | 
| 4 | 2, 3 | anbi12d 632 | . . . . 5
⊢ (𝐹 Fn ω → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))) | 
| 5 | 4 | 3ad2ant1 1133 | . . . 4
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐))) | 
| 6 |  | reeanv 3228 | . . . . 5
⊢
(∃𝑑 ∈
ω ∃𝑒 ∈
ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) ↔ (∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐)) | 
| 7 |  | nnord 7896 | . . . . . . . . . . 11
⊢ (𝑑 ∈ ω → Ord 𝑑) | 
| 8 |  | nnord 7896 | . . . . . . . . . . 11
⊢ (𝑒 ∈ ω → Ord 𝑒) | 
| 9 |  | ordtri2or2 6482 | . . . . . . . . . . 11
⊢ ((Ord
𝑑 ∧ Ord 𝑒) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑)) | 
| 10 | 7, 8, 9 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑑 ∈ ω ∧ 𝑒 ∈ ω) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑)) | 
| 11 | 10 | adantl 481 | . . . . . . . . 9
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑)) | 
| 12 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑑 ∈ V | 
| 13 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑒 ∈ V | 
| 14 |  | eleq1w 2823 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑑 → (𝑏 ∈ ω ↔ 𝑑 ∈ ω)) | 
| 15 |  | eleq1w 2823 | . . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → (𝑐 ∈ ω ↔ 𝑒 ∈ ω)) | 
| 16 | 14, 15 | bi2anan9 638 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑑 ∈ ω ∧ 𝑒 ∈ ω))) | 
| 17 | 16 | anbi2d 630 | . . . . . . . . . . . 12
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)))) | 
| 18 |  | sseq12 4010 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (𝑏 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑒)) | 
| 19 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑)) | 
| 20 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑒 → (𝐹‘𝑐) = (𝐹‘𝑒)) | 
| 21 | 19, 20 | breqan12d 5158 | . . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑒))) | 
| 22 | 19, 20 | eqeqan12d 2750 | . . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑑) = (𝐹‘𝑒))) | 
| 23 | 21, 22 | orbi12d 918 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)))) | 
| 24 | 18, 23 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒))))) | 
| 25 | 17, 24 | imbi12d 344 | . . . . . . . . . . 11
⊢ ((𝑏 = 𝑑 ∧ 𝑐 = 𝑒) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)))))) | 
| 26 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑏 → (𝐹‘𝑑) = (𝐹‘𝑏)) | 
| 27 | 26 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑏))) | 
| 28 | 26 | eqeq2d 2747 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑏 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑏))) | 
| 29 | 27, 28 | orbi12d 918 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑏 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)))) | 
| 30 | 29 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑏 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏))))) | 
| 31 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑒 → (𝐹‘𝑑) = (𝐹‘𝑒)) | 
| 32 | 31 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) | 
| 33 | 31 | eqeq2d 2747 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑒))) | 
| 34 | 32, 33 | orbi12d 918 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)))) | 
| 35 | 34 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))))) | 
| 36 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = suc 𝑒 → (𝐹‘𝑑) = (𝐹‘suc 𝑒)) | 
| 37 | 36 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))) | 
| 38 | 36 | eqeq2d 2747 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = suc 𝑒 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒))) | 
| 39 | 37, 38 | orbi12d 918 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = suc 𝑒 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 40 | 39 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = suc 𝑒 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 41 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐)) | 
| 42 | 41 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ↔ (𝐹‘𝑏)𝑅(𝐹‘𝑐))) | 
| 43 | 41 | eqeq2d 2747 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑐 → ((𝐹‘𝑏) = (𝐹‘𝑑) ↔ (𝐹‘𝑏) = (𝐹‘𝑐))) | 
| 44 | 42, 43 | orbi12d 918 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑐 → (((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) | 
| 45 | 44 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑐 → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑏) = (𝐹‘𝑑))) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))))) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑏) = (𝐹‘𝑏) | 
| 47 | 46 | olci 866 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)) | 
| 48 | 47 | 2a1i 12 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ω → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑏) = (𝐹‘𝑏)))) | 
| 49 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑒 → (𝐹‘𝑎) = (𝐹‘𝑒)) | 
| 50 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑒 → suc 𝑎 = suc 𝑒) | 
| 51 | 50 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑒 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑒)) | 
| 52 | 49, 51 | breq12d 5155 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) | 
| 53 | 49, 51 | eqeq12d 2752 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑒 → ((𝐹‘𝑎) = (𝐹‘suc 𝑎) ↔ (𝐹‘𝑒) = (𝐹‘suc 𝑒))) | 
| 54 | 52, 53 | orbi12d 918 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑒 → (((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)))) | 
| 55 |  | simpr2 1195 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎))) | 
| 56 |  | simplll 774 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω) | 
| 57 | 54, 55, 56 | rspcdva 3622 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒))) | 
| 58 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑅 Po ran 𝐹) | 
| 59 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝐹 Fn ω) | 
| 60 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑏 ∈ ω) | 
| 61 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 Fn ω ∧ 𝑏 ∈ ω) → (𝐹‘𝑏) ∈ ran 𝐹) | 
| 62 | 59, 60, 61 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑏) ∈ ran 𝐹) | 
| 63 |  | simplll 774 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → 𝑒 ∈ ω) | 
| 64 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 Fn ω ∧ 𝑒 ∈ ω) → (𝐹‘𝑒) ∈ ran 𝐹) | 
| 65 | 59, 63, 64 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘𝑒) ∈ ran 𝐹) | 
| 66 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑒 ∈ ω → suc 𝑒 ∈
ω) | 
| 67 | 66 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → suc 𝑒 ∈ ω) | 
| 68 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 Fn ω ∧ suc 𝑒 ∈ ω) → (𝐹‘suc 𝑒) ∈ ran 𝐹) | 
| 69 | 59, 67, 68 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (𝐹‘suc 𝑒) ∈ ran 𝐹) | 
| 70 |  | potr 5604 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 Po ran 𝐹 ∧ ((𝐹‘𝑏) ∈ ran 𝐹 ∧ (𝐹‘𝑒) ∈ ran 𝐹 ∧ (𝐹‘suc 𝑒) ∈ ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))) | 
| 71 | 58, 62, 65, 69, 70 | syl13anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))) | 
| 72 | 71 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑒 ∈
ω ∧ 𝑏 ∈
ω) ∧ 𝑏 ⊆
𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)) | 
| 73 | 72 | ancom2s 650 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑒 ∈
ω ∧ 𝑏 ∈
ω) ∧ 𝑏 ⊆
𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒)) | 
| 74 | 73 | orcd 873 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑒 ∈
ω ∧ 𝑏 ∈
ω) ∧ 𝑏 ⊆
𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑒))) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))) | 
| 75 | 74 | expr 456 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑒 ∈
ω ∧ 𝑏 ∈
ω) ∧ 𝑏 ⊆
𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 76 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ↔ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒))) | 
| 77 | 76 | biimprcd 250 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))) | 
| 78 |  | orc 867 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))) | 
| 79 | 77, 78 | syl6 35 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑒 ∈
ω ∧ 𝑏 ∈
ω) ∧ 𝑏 ⊆
𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → ((𝐹‘𝑏) = (𝐹‘𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 81 | 75, 80 | jaod 859 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑒 ∈
ω ∧ 𝑏 ∈
ω) ∧ 𝑏 ⊆
𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) ∧ (𝐹‘𝑒)𝑅(𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 82 | 81 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 83 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑏)𝑅(𝐹‘suc 𝑒))) | 
| 84 |  | eqeq2 2748 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → ((𝐹‘𝑏) = (𝐹‘𝑒) ↔ (𝐹‘𝑏) = (𝐹‘suc 𝑒))) | 
| 85 | 83, 84 | orbi12d 918 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) ↔ ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 86 | 85 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 87 | 86 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → ((𝐹‘𝑒) = (𝐹‘suc 𝑒) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 88 | 82, 87 | jaod 859 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 89 | 88 | 3adantr2 1170 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑒)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑒) = (𝐹‘suc 𝑒)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 90 | 57, 89 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) ∧ (𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹)) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒)))) | 
| 91 | 90 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒)) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 92 | 91 | a2d 29 | . . . . . . . . . . . . . . 15
⊢ (((𝑒 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑒) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑏) = (𝐹‘𝑒))) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘suc 𝑒) ∨ (𝐹‘𝑏) = (𝐹‘suc 𝑒))))) | 
| 93 | 30, 35, 40, 45, 48, 92 | findsg 7920 | . . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) | 
| 94 | 93 | ancom1s 653 | . . . . . . . . . . . . 13
⊢ (((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐) → ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) | 
| 95 | 94 | impcom 407 | . . . . . . . . . . . 12
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ∧ 𝑏 ⊆ 𝑐)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) | 
| 96 | 95 | expr 456 | . . . . . . . . . . 11
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) | 
| 97 | 12, 13, 25, 96 | vtocl2 3565 | . . . . . . . . . 10
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑑 ⊆ 𝑒 → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)))) | 
| 98 |  | eleq1w 2823 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑒 → (𝑏 ∈ ω ↔ 𝑒 ∈ ω)) | 
| 99 |  | eleq1w 2823 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑑 → (𝑐 ∈ ω ↔ 𝑑 ∈ ω)) | 
| 100 | 98, 99 | bi2anan9 638 | . . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) ↔ (𝑒 ∈ ω ∧ 𝑑 ∈ ω))) | 
| 101 | 100 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) ↔ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)))) | 
| 102 |  | sseq12 4010 | . . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (𝑏 ⊆ 𝑐 ↔ 𝑒 ⊆ 𝑑)) | 
| 103 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑒 → (𝐹‘𝑏) = (𝐹‘𝑒)) | 
| 104 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑑 → (𝐹‘𝑐) = (𝐹‘𝑑)) | 
| 105 | 103, 104 | breqan12d 5158 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ↔ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 106 | 103, 104 | eqeqan12d 2750 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝐹‘𝑏) = (𝐹‘𝑐) ↔ (𝐹‘𝑒) = (𝐹‘𝑑))) | 
| 107 | 105, 106 | orbi12d 918 | . . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → (((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)) ↔ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))) | 
| 108 | 102, 107 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐))) ↔ (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))) | 
| 109 | 101, 108 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((𝑏 = 𝑒 ∧ 𝑐 = 𝑑) → ((((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑏 ∈ ω ∧ 𝑐 ∈ ω)) → (𝑏 ⊆ 𝑐 → ((𝐹‘𝑏)𝑅(𝐹‘𝑐) ∨ (𝐹‘𝑏) = (𝐹‘𝑐)))) ↔ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))))) | 
| 110 | 13, 12, 109, 96 | vtocl2 3565 | . . . . . . . . . . 11
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))) | 
| 111 | 110 | ancom2s 650 | . . . . . . . . . 10
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (𝑒 ⊆ 𝑑 → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))) | 
| 112 | 97, 111 | orim12d 966 | . . . . . . . . 9
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑑 ⊆ 𝑒 ∨ 𝑒 ⊆ 𝑑) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))))) | 
| 113 | 11, 112 | mpd 15 | . . . . . . . 8
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)))) | 
| 114 |  | 3mix1 1330 | . . . . . . . . . 10
⊢ ((𝐹‘𝑑)𝑅(𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 115 |  | 3mix2 1331 | . . . . . . . . . 10
⊢ ((𝐹‘𝑑) = (𝐹‘𝑒) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 116 | 114, 115 | jaoi 857 | . . . . . . . . 9
⊢ (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 117 |  | 3mix3 1332 | . . . . . . . . . 10
⊢ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 118 | 115 | eqcoms 2744 | . . . . . . . . . 10
⊢ ((𝐹‘𝑒) = (𝐹‘𝑑) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 119 | 117, 118 | jaoi 857 | . . . . . . . . 9
⊢ (((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 120 | 116, 119 | jaoi 857 | . . . . . . . 8
⊢ ((((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒)) ∨ ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ∨ (𝐹‘𝑒) = (𝐹‘𝑑))) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 121 | 113, 120 | syl 17 | . . . . . . 7
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑))) | 
| 122 |  | breq12 5147 | . . . . . . . 8
⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑)𝑅(𝐹‘𝑒) ↔ 𝑏𝑅𝑐)) | 
| 123 |  | eqeq12 2753 | . . . . . . . 8
⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑑) = (𝐹‘𝑒) ↔ 𝑏 = 𝑐)) | 
| 124 |  | breq12 5147 | . . . . . . . . 9
⊢ (((𝐹‘𝑒) = 𝑐 ∧ (𝐹‘𝑑) = 𝑏) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏)) | 
| 125 | 124 | ancoms 458 | . . . . . . . 8
⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → ((𝐹‘𝑒)𝑅(𝐹‘𝑑) ↔ 𝑐𝑅𝑏)) | 
| 126 | 122, 123,
125 | 3orbi123d 1436 | . . . . . . 7
⊢ (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (((𝐹‘𝑑)𝑅(𝐹‘𝑒) ∨ (𝐹‘𝑑) = (𝐹‘𝑒) ∨ (𝐹‘𝑒)𝑅(𝐹‘𝑑)) ↔ (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))) | 
| 127 | 121, 126 | syl5ibcom 245 | . . . . . 6
⊢ (((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) ∧ (𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → (((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))) | 
| 128 | 127 | rexlimdvva 3212 | . . . . 5
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → (∃𝑑 ∈ ω ∃𝑒 ∈ ω ((𝐹‘𝑑) = 𝑏 ∧ (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))) | 
| 129 | 6, 128 | biimtrrid 243 | . . . 4
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((∃𝑑 ∈ ω (𝐹‘𝑑) = 𝑏 ∧ ∃𝑒 ∈ ω (𝐹‘𝑒) = 𝑐) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))) | 
| 130 | 5, 129 | sylbid 240 | . . 3
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ((𝑏 ∈ ran 𝐹 ∧ 𝑐 ∈ ran 𝐹) → (𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))) | 
| 131 | 130 | ralrimivv 3199 | . 2
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏)) | 
| 132 |  | df-so 5592 | . 2
⊢ (𝑅 Or ran 𝐹 ↔ (𝑅 Po ran 𝐹 ∧ ∀𝑏 ∈ ran 𝐹∀𝑐 ∈ ran 𝐹(𝑏𝑅𝑐 ∨ 𝑏 = 𝑐 ∨ 𝑐𝑅𝑏))) | 
| 133 | 1, 131, 132 | sylanbrc 583 | 1
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹) |