| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relco 6125 | . 2
⊢ Rel
(t++𝑅 ∘ t++𝑅) | 
| 2 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑛 ∈ (ω ∖
1o) → 𝑛
∈ ω) | 
| 3 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑚 ∈ (ω ∖
1o) → 𝑚
∈ ω) | 
| 4 |  | nnacl 8650 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈
ω) | 
| 5 | 2, 3, 4 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω) | 
| 6 |  | eldif 3960 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ω ∖
1o) ↔ (𝑛
∈ ω ∧ ¬ 𝑛 ∈ 1o)) | 
| 7 |  | 1on 8519 | . . . . . . . . . . . . . . . 16
⊢
1o ∈ On | 
| 8 | 7 | onordi 6494 | . . . . . . . . . . . . . . 15
⊢ Ord
1o | 
| 9 |  | nnord 7896 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → Ord 𝑛) | 
| 10 |  | ordtri1 6416 | . . . . . . . . . . . . . . 15
⊢ ((Ord
1o ∧ Ord 𝑛)
→ (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o)) | 
| 11 | 8, 9, 10 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(1o ⊆ 𝑛
↔ ¬ 𝑛 ∈
1o)) | 
| 12 | 11 | biimpar 477 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ω ∧ ¬
𝑛 ∈ 1o)
→ 1o ⊆ 𝑛) | 
| 13 | 6, 12 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ (ω ∖
1o) → 1o ⊆ 𝑛) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 1o ⊆ 𝑛) | 
| 15 |  | nnaword1 8668 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚)) | 
| 16 | 2, 3, 15 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚)) | 
| 17 | 14, 16 | sstrd 3993 | . . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚)) | 
| 18 |  | nnord 7896 | . . . . . . . . . . . 12
⊢ ((𝑛 +o 𝑚) ∈ ω → Ord
(𝑛 +o 𝑚)) | 
| 19 | 5, 18 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚)) | 
| 20 |  | ordtri1 6416 | . . . . . . . . . . 11
⊢ ((Ord
1o ∧ Ord (𝑛
+o 𝑚)) →
(1o ⊆ (𝑛
+o 𝑚) ↔
¬ (𝑛 +o
𝑚) ∈
1o)) | 
| 21 | 8, 19, 20 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈
1o)) | 
| 22 | 17, 21 | mpbid 232 | . . . . . . . . 9
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o) | 
| 23 | 5, 22 | eldifd 3961 | . . . . . . . 8
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖
1o)) | 
| 24 |  | 0elsuc 7856 | . . . . . . . . . . . . 13
⊢ (Ord
(𝑛 +o 𝑚) → ∅ ∈ suc
(𝑛 +o 𝑚)) | 
| 25 | 19, 24 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚)) | 
| 26 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛)) | 
| 27 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = ∅ → (𝑓‘𝑝) = (𝑓‘∅)) | 
| 28 |  | eqeq2 2748 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅)) | 
| 29 | 28 | riotabidv 7391 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = ∅ →
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) | 
| 30 | 29 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑝 = ∅ → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) | 
| 31 | 26, 27, 30 | ifbieq12d 4553 | . . . . . . . . . . . . 13
⊢ (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))) | 
| 32 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) | 
| 33 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑓‘∅) ∈
V | 
| 34 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈
V | 
| 35 | 33, 34 | ifex 4575 | . . . . . . . . . . . . 13
⊢
if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V | 
| 36 | 31, 32, 35 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (∅
∈ suc (𝑛 +o
𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc
𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))) | 
| 37 | 25, 36 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc
𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))) | 
| 38 | 2 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 𝑛 ∈ ω) | 
| 39 | 38, 9 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → Ord 𝑛) | 
| 40 |  | 0elsuc 7856 | . . . . . . . . . . . . 13
⊢ (Ord
𝑛 → ∅ ∈ suc
𝑛) | 
| 41 | 39, 40 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛) | 
| 42 | 41 | iftrued 4532 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅)) | 
| 43 | 37, 42 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅)) | 
| 44 |  | simpl2l 1226 | . . . . . . . . . 10
⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘∅) = 𝑥) | 
| 45 | 43, 44 | sylan9eq 2796 | . . . . . . . . 9
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥) | 
| 46 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (𝑛 +o 𝑚) ∈ V | 
| 47 | 46 | sucid 6465 | . . . . . . . . . . . 12
⊢ (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚) | 
| 48 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛)) | 
| 49 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑓‘𝑝) = (𝑓‘(𝑛 +o 𝑚))) | 
| 50 |  | eqeq2 2748 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) | 
| 51 | 50 | riotabidv 7391 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = (𝑛 +o 𝑚) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) | 
| 52 | 51 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) | 
| 53 | 48, 49, 52 | ifbieq12d 4553 | . . . . . . . . . . . . 13
⊢ (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))) | 
| 54 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑓‘(𝑛 +o 𝑚)) ∈ V | 
| 55 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V | 
| 56 | 54, 55 | ifex 4575 | . . . . . . . . . . . . 13
⊢ if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V | 
| 57 | 53, 32, 56 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ ((𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))) | 
| 58 | 47, 57 | mp1i 13 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))) | 
| 59 |  | df-1o 8507 | . . . . . . . . . . . . . . . . . 18
⊢
1o = suc ∅ | 
| 60 | 59 | difeq2i 4122 | . . . . . . . . . . . . . . . . 17
⊢ (ω
∖ 1o) = (ω ∖ suc ∅) | 
| 61 | 60 | eleq2i 2832 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (ω ∖
1o) ↔ 𝑛
∈ (ω ∖ suc ∅)) | 
| 62 |  | peano1 7911 | . . . . . . . . . . . . . . . . 17
⊢ ∅
∈ ω | 
| 63 |  | eldifsucnn 8703 | . . . . . . . . . . . . . . . . 17
⊢ (∅
∈ ω → (𝑛
∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)) | 
| 64 | 62, 63 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (ω ∖ suc
∅) ↔ ∃𝑥
∈ (ω ∖ ∅)𝑛 = suc 𝑥) | 
| 65 |  | dif0 4377 | . . . . . . . . . . . . . . . . 17
⊢ (ω
∖ ∅) = ω | 
| 66 | 65 | rexeqi 3324 | . . . . . . . . . . . . . . . 16
⊢
(∃𝑥 ∈
(ω ∖ ∅)𝑛
= suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥) | 
| 67 | 61, 64, 66 | 3bitri 297 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ω ∖
1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥) | 
| 68 | 60 | eleq2i 2832 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (ω ∖
1o) ↔ 𝑚
∈ (ω ∖ suc ∅)) | 
| 69 |  | eldifsucnn 8703 | . . . . . . . . . . . . . . . . 17
⊢ (∅
∈ ω → (𝑚
∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)) | 
| 70 | 62, 69 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (ω ∖ suc
∅) ↔ ∃𝑦
∈ (ω ∖ ∅)𝑚 = suc 𝑦) | 
| 71 | 65 | rexeqi 3324 | . . . . . . . . . . . . . . . 16
⊢
(∃𝑦 ∈
(ω ∖ ∅)𝑚
= suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦) | 
| 72 | 68, 70, 71 | 3bitri 297 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (ω ∖
1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦) | 
| 73 | 67, 72 | anbi12i 628 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)) | 
| 74 |  | reeanv 3228 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ω ∃𝑦 ∈
ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)) | 
| 75 | 73, 74 | bitr4i 278 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦)) | 
| 76 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) | 
| 77 |  | nnaword1 8668 | . . . . . . . . . . . . . . . . . . 19
⊢ ((suc
𝑥 ∈ ω ∧
𝑦 ∈ ω) →
suc 𝑥 ⊆ (suc 𝑥 +o 𝑦)) | 
| 78 | 76, 77 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc
𝑥 ⊆ (suc 𝑥 +o 𝑦)) | 
| 79 | 76 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc
𝑥 ∈
ω) | 
| 80 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑥 ∈ ω → Ord
suc 𝑥) | 
| 81 | 79, 80 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc
𝑥) | 
| 82 |  | nnacl 8650 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((suc
𝑥 ∈ ω ∧
𝑦 ∈ ω) →
(suc 𝑥 +o 𝑦) ∈
ω) | 
| 83 | 76, 82 | sylan 580 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝑥 +o 𝑦) ∈
ω) | 
| 84 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((suc
𝑥 +o 𝑦) ∈ ω → Ord (suc
𝑥 +o 𝑦)) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc
𝑥 +o 𝑦)) | 
| 86 |  | ordsucsssuc 7844 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Ord suc
𝑥 ∧ Ord (suc 𝑥 +o 𝑦)) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))) | 
| 87 | 81, 85, 86 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))) | 
| 88 | 78, 87 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc
𝑥 ⊆ suc (suc 𝑥 +o 𝑦)) | 
| 89 |  | nnasuc 8645 | . . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑥 ∈ ω ∧
𝑦 ∈ ω) →
(suc 𝑥 +o suc
𝑦) = suc (suc 𝑥 +o 𝑦)) | 
| 90 | 76, 89 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦)) | 
| 91 | 88, 90 | sseqtrrd 4020 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc
𝑥 ⊆ (suc 𝑥 +o suc 𝑦)) | 
| 92 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑥 ∈ ω → suc
suc 𝑥 ∈
ω) | 
| 93 | 79, 92 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc
𝑥 ∈
ω) | 
| 94 |  | nnord 7896 | . . . . . . . . . . . . . . . . . 18
⊢ (suc suc
𝑥 ∈ ω → Ord
suc suc 𝑥) | 
| 95 | 93, 94 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc
suc 𝑥) | 
| 96 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) | 
| 97 |  | nnacl 8650 | . . . . . . . . . . . . . . . . . . 19
⊢ ((suc
𝑥 ∈ ω ∧ suc
𝑦 ∈ ω) →
(suc 𝑥 +o suc
𝑦) ∈
ω) | 
| 98 | 76, 96, 97 | syl2an 596 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝑥 +o suc 𝑦) ∈
ω) | 
| 99 |  | nnord 7896 | . . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑥 +o suc 𝑦) ∈ ω → Ord (suc
𝑥 +o suc 𝑦)) | 
| 100 | 98, 99 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc
𝑥 +o suc 𝑦)) | 
| 101 |  | ordtri1 6416 | . . . . . . . . . . . . . . . . 17
⊢ ((Ord suc
suc 𝑥 ∧ Ord (suc 𝑥 +o suc 𝑦)) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)) | 
| 102 | 95, 100, 101 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc suc
𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)) | 
| 103 | 91, 102 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬
(suc 𝑥 +o suc
𝑦) ∈ suc suc 𝑥) | 
| 104 |  | oveq12 7441 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦)) | 
| 105 |  | suceq 6449 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥) | 
| 107 | 104, 106 | eleq12d 2834 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ((𝑛 +o 𝑚) ∈ suc 𝑛 ↔ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)) | 
| 108 | 107 | notbid 318 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (¬ (𝑛 +o 𝑚) ∈ suc 𝑛 ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)) | 
| 109 | 103, 108 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)) | 
| 110 | 109 | rexlimivv 3200 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ω ∃𝑦 ∈
ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛) | 
| 111 | 75, 110 | sylbi 217 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛) | 
| 112 | 111 | iffalsed 4535 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) | 
| 113 | 3 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 𝑚 ∈ ω) | 
| 114 | 38 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑛 ∈ ω) | 
| 115 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑞 ∈ ω) | 
| 116 | 113 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑚 ∈ ω) | 
| 117 |  | nnacan 8667 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚)) | 
| 118 | 114, 115,
116, 117 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚)) | 
| 119 | 113, 118 | riota5 7418 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚) | 
| 120 | 119 | fveq2d 6909 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔‘𝑚)) | 
| 121 | 58, 112, 120 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔‘𝑚)) | 
| 122 |  | simpr2r 1233 | . . . . . . . . . 10
⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘𝑚) = 𝑦) | 
| 123 | 121, 122 | sylan9eq 2796 | . . . . . . . . 9
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) | 
| 124 |  | simprl3 1220 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) | 
| 125 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐)) | 
| 126 |  | suceq 6449 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐) | 
| 127 | 126 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐)) | 
| 128 | 125, 127 | breq12d 5155 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐))) | 
| 129 | 128 | rspcv 3617 | . . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝑛 → (∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐))) | 
| 130 | 124, 129 | mpan9 506 | . . . . . . . . . . . . . 14
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)) | 
| 131 |  | elelsuc 6456 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ 𝑛 → 𝑐 ∈ suc 𝑛) | 
| 132 | 131 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → 𝑐 ∈ suc 𝑛) | 
| 133 | 132 | iftrued 4532 | . . . . . . . . . . . . . 14
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑐)) | 
| 134 |  | ordsucelsuc 7843 | . . . . . . . . . . . . . . . . . 18
⊢ (Ord
𝑛 → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛)) | 
| 135 | 39, 134 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛)) | 
| 136 | 135 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛)) | 
| 137 | 136 | biimpa 476 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → suc 𝑐 ∈ suc 𝑛) | 
| 138 | 137 | iftrued 4532 | . . . . . . . . . . . . . 14
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐)) | 
| 139 | 130, 133,
138 | 3brtr4d 5174 | . . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 140 | 139 | adantlr 715 | . . . . . . . . . . . 12
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 141 | 39 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord 𝑛) | 
| 142 | 5 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 +o 𝑚) ∈ ω) | 
| 143 |  | elnn 7899 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω) | 
| 144 | 143 | ancoms 458 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω) | 
| 145 | 142, 144 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω) | 
| 146 |  | nnord 7896 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ ω → Ord 𝑐) | 
| 147 | 145, 146 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐) | 
| 148 |  | ordtri3or 6415 | . . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝑛 ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛)) | 
| 149 | 141, 147,
148 | syl2an2r 685 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛)) | 
| 150 |  | 3orel3 1487 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑐 ∈ 𝑛 → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐))) | 
| 151 | 149, 150 | syl5com 31 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐))) | 
| 152 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘𝑏) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 153 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 154 | 153 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 155 | 152, 154 | breq12d 5155 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))) | 
| 156 |  | simprr3 1223 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) | 
| 157 | 156 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) | 
| 159 |  | ordelss 6399 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Ord
𝑐 ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐) | 
| 160 | 147, 159 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐) | 
| 161 | 38 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → 𝑛 ∈ ω) | 
| 162 | 161 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑛 ∈ ω) | 
| 163 | 145 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑐 ∈ ω) | 
| 164 |  | nnawordex 8676 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 165 | 162, 163,
164 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 166 | 160, 165 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) | 
| 167 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝)) | 
| 168 | 167 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐)) | 
| 169 | 168 | cbvrexvw 3237 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐) | 
| 170 | 166, 169 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐) | 
| 171 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐) | 
| 172 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑐 ∈ (𝑛 +o 𝑚)) | 
| 173 | 171, 172 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)) | 
| 174 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω) | 
| 175 | 3 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑚 ∈ ω) | 
| 176 | 175 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑚 ∈ ω) | 
| 177 | 162 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ ω) | 
| 178 | 177 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑛 ∈ ω) | 
| 179 |  | nnaord 8658 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))) | 
| 180 | 174, 176,
178, 179 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))) | 
| 181 | 173, 180 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ 𝑚) | 
| 182 | 170, 181,
171 | reximssdv 3172 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐) | 
| 183 |  | elnn 7899 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ 𝑚 ∧ 𝑚 ∈ ω) → 𝑝 ∈ ω) | 
| 184 | 183 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω) | 
| 185 | 175, 184 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω) | 
| 186 |  | nnasmo 8702 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ ω →
∃*𝑞 ∈ ω
(𝑛 +o 𝑞) = 𝑐) | 
| 187 | 177, 186 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) | 
| 188 |  | reu5 3381 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃!𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 189 | 166, 187,
188 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) | 
| 190 | 189 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) | 
| 191 | 168 | riota2 7414 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ ω ∧
∃!𝑞 ∈ ω
(𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝)) | 
| 192 | 185, 190,
191 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝)) | 
| 193 |  | eqcom 2743 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((℩𝑞
∈ ω (𝑛
+o 𝑞) = 𝑐) = 𝑝 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 194 | 192, 193 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 195 | 194 | rexbidva 3176 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 196 | 182, 195 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 197 |  | risset 3232 | . . . . . . . . . . . . . . . . . . . 20
⊢
((℩𝑞
∈ ω (𝑛
+o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 198 | 196, 197 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚) | 
| 199 | 155, 158,
198 | rspcdva 3622 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 200 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ 𝑐) | 
| 201 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑛 ∈ V | 
| 202 | 147 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → Ord 𝑐) | 
| 203 |  | ordelsuc 7841 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐)) | 
| 204 | 201, 202,
203 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐)) | 
| 205 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) | 
| 206 | 38, 205 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω) | 
| 207 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (suc
𝑛 ∈ ω → Ord
suc 𝑛) | 
| 208 | 206, 207 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → Ord suc 𝑛) | 
| 209 | 208 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord suc 𝑛) | 
| 210 | 209 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord suc 𝑛) | 
| 211 |  | ordtri1 6416 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Ord suc
𝑛 ∧ Ord 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛)) | 
| 212 | 210, 202,
211 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛)) | 
| 213 | 204, 212 | bitrd 279 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛)) | 
| 214 | 200, 213 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ¬ 𝑐 ∈ suc 𝑛) | 
| 215 | 214 | iffalsed 4535 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 216 |  | riotacl 7406 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃!𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) | 
| 217 | 189, 216 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) | 
| 218 |  | nnasuc 8645 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ω ∧
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 219 | 162, 217,
218 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 220 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 221 |  | nfriota1 7396 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑞(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) | 
| 222 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑞𝑛 | 
| 223 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑞
+o | 
| 224 | 222, 223,
221 | nfov 7462 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 225 | 224 | nfeq1 2920 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑞(𝑛 +o
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐)) = 𝑐 | 
| 226 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 227 | 226 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐)) | 
| 228 | 221, 225,
227 | riota2f 7413 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((℩𝑞
∈ ω (𝑛
+o 𝑞) = 𝑐) ∈ ω ∧
∃!𝑞 ∈ ω
(𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 229 | 217, 189,
228 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 230 | 220, 229 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐) | 
| 231 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 +o
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐)) = 𝑐 → suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐) | 
| 232 | 230, 231 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐) | 
| 233 | 219, 232 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐) | 
| 234 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((℩𝑞
∈ ω (𝑛
+o 𝑞) = 𝑐) ∈ ω → suc
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐) ∈ ω) | 
| 235 | 217, 234 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) | 
| 236 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 ∈ ω → suc 𝑝 ∈
ω) | 
| 237 |  | nnasuc 8645 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) | 
| 238 | 177, 237 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) | 
| 239 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝)) | 
| 240 | 239 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))) | 
| 241 | 240 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((suc
𝑝 ∈ ω ∧
(𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝)) | 
| 242 | 236, 238,
241 | syl2an2 686 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝)) | 
| 243 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐) | 
| 244 | 243 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐)) | 
| 245 | 244 | rexbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) | 
| 246 | 242, 245 | syl5ibcom 245 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ((𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) | 
| 247 | 246 | rexlimdva 3154 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) | 
| 248 | 170, 247 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) | 
| 249 |  | nnasmo 8702 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ω →
∃*𝑞 ∈ ω
(𝑛 +o 𝑞) = suc 𝑐) | 
| 250 | 177, 249 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) | 
| 251 |  | reu5 3381 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃!𝑞 ∈
ω (𝑛 +o
𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) | 
| 252 | 248, 250,
251 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) | 
| 253 | 221 | nfsuc 6455 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑞 suc
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐) | 
| 254 | 222, 223,
253 | nfov 7462 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 255 | 254 | nfeq1 2920 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑞(𝑛 +o suc
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐)) = suc 𝑐 | 
| 256 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 257 | 256 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)) | 
| 258 | 253, 255,
257 | riota2f 7413 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((suc
(℩𝑞 ∈
ω (𝑛 +o
𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 259 | 235, 252,
258 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 260 | 233, 259 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 261 | 260 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 262 | 199, 215,
261 | 3brtr4d 5174 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) | 
| 263 | 262 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 264 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = ∅ → (𝑔‘𝑏) = (𝑔‘∅)) | 
| 265 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅) | 
| 266 | 265, 59 | eqtr4di 2794 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = ∅ → suc 𝑏 =
1o) | 
| 267 | 266 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o)) | 
| 268 | 264, 267 | breq12d 5155 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = ∅ → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o))) | 
| 269 |  | eldif 3960 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ (ω ∖
1o) ↔ (𝑚
∈ ω ∧ ¬ 𝑚 ∈ 1o)) | 
| 270 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ ω → Ord 𝑚) | 
| 271 |  | ordtri1 6416 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
1o ∧ Ord 𝑚)
→ (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o)) | 
| 272 | 8, 270, 271 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ ω →
(1o ⊆ 𝑚
↔ ¬ 𝑚 ∈
1o)) | 
| 273 | 272 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ ω ∧ ¬
𝑚 ∈ 1o)
→ 1o ⊆ 𝑚) | 
| 274 | 269, 273 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (ω ∖
1o) → 1o ⊆ 𝑚) | 
| 275 | 274 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 1o ⊆ 𝑚) | 
| 276 | 59, 275 | eqsstrrid 4022 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚) | 
| 277 |  | 0ex 5306 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∅
∈ V | 
| 278 | 113, 270 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → Ord 𝑚) | 
| 279 |  | ordelsuc 7841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((∅
∈ V ∧ Ord 𝑚)
→ (∅ ∈ 𝑚
↔ suc ∅ ⊆ 𝑚)) | 
| 280 | 277, 278,
279 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆
𝑚)) | 
| 281 | 276, 280 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ∅ ∈ 𝑚) | 
| 282 | 281 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∅ ∈ 𝑚) | 
| 283 | 268, 156,
282 | rspcdva 3622 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘∅)𝑅(𝑔‘1o)) | 
| 284 |  | simpl2r 1227 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = 𝑧) | 
| 285 |  | simpr2l 1232 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘∅) = 𝑧) | 
| 286 | 284, 285 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = (𝑔‘∅)) | 
| 287 | 286 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛) = (𝑔‘∅)) | 
| 288 |  | nnon 7894 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → 𝑛 ∈ On) | 
| 289 | 38, 288 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → 𝑛 ∈ On) | 
| 290 |  | oa1suc 8570 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ On → (𝑛 +o 1o) =
suc 𝑛) | 
| 291 | 289, 290 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛) | 
| 292 |  | 1onn 8679 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
1o ∈ ω | 
| 293 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o
1o)) | 
| 294 | 293 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛)) | 
| 295 | 294 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) | 
| 296 | 292, 291,
295 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) | 
| 297 |  | nnasmo 8702 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ω →
∃*𝑞 ∈ ω
(𝑛 +o 𝑞) = suc 𝑛) | 
| 298 | 38, 297 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) | 
| 299 |  | reu5 3381 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃!𝑞 ∈
ω (𝑛 +o
𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) | 
| 300 | 296, 298,
299 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) | 
| 301 | 294 | riota2 7414 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1o ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)) | 
| 302 | 292, 300,
301 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)) | 
| 303 | 291, 302 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o) | 
| 304 | 303 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o) | 
| 305 | 304 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o)) | 
| 306 | 283, 287,
305 | 3brtr4d 5174 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))) | 
| 307 | 201 | sucid 6465 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ suc 𝑛 | 
| 308 | 307 | iftruei 4531 | . . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑛) | 
| 309 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛)) | 
| 310 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = (𝑓‘𝑐)) | 
| 311 | 309, 310 | ifbieq1d 4549 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))) | 
| 312 | 308, 311 | eqtr3id 2790 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))) | 
| 313 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐) | 
| 314 | 313 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐)) | 
| 315 | 314 | riotabidv 7391 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) | 
| 316 | 315 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) | 
| 317 | 312, 316 | breq12d 5155 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑐 → ((𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) ↔ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 318 | 306, 317 | syl5ibcom 245 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 319 | 318 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 320 | 263, 319 | jaod 859 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 321 | 151, 320 | syld 47 | . . . . . . . . . . . . . 14
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 322 | 321 | imp 406 | . . . . . . . . . . . . 13
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) | 
| 323 | 135 | notbid 318 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛)) | 
| 324 | 323 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛)) | 
| 325 | 324 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛)) | 
| 326 | 325 | biimpa 476 | . . . . . . . . . . . . . 14
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → ¬ suc 𝑐 ∈ suc 𝑛) | 
| 327 | 326 | iffalsed 4535 | . . . . . . . . . . . . 13
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) | 
| 328 | 322, 327 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢
(((((𝑛 ∈
(ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o))
∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 329 | 140, 328 | pm2.61dan 812 | . . . . . . . . . . 11
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 330 |  | elelsuc 6456 | . . . . . . . . . . . . 13
⊢ (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚)) | 
| 331 | 330 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚)) | 
| 332 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛)) | 
| 333 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑐 → (𝑓‘𝑝) = (𝑓‘𝑐)) | 
| 334 |  | eqeq2 2748 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐)) | 
| 335 | 334 | riotabidv 7391 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) | 
| 336 | 335 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) | 
| 337 | 332, 333,
336 | ifbieq12d 4553 | . . . . . . . . . . . . 13
⊢ (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))) | 
| 338 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑓‘𝑐) ∈ V | 
| 339 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V | 
| 340 | 338, 339 | ifex 4575 | . . . . . . . . . . . . 13
⊢ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V | 
| 341 | 337, 32, 340 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))) | 
| 342 | 331, 341 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))) | 
| 343 |  | ordsucelsuc 7843 | . . . . . . . . . . . . . . 15
⊢ (Ord
(𝑛 +o 𝑚) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚))) | 
| 344 | 19, 343 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚))) | 
| 345 | 344 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚))) | 
| 346 | 345 | biimpa 476 | . . . . . . . . . . . 12
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → suc 𝑐 ∈ suc (𝑛 +o 𝑚)) | 
| 347 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛)) | 
| 348 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = suc 𝑐 → (𝑓‘𝑝) = (𝑓‘suc 𝑐)) | 
| 349 |  | eqeq2 2748 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐)) | 
| 350 | 349 | riotabidv 7391 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = suc 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) | 
| 351 | 350 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑝 = suc 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) | 
| 352 | 347, 348,
351 | ifbieq12d 4553 | . . . . . . . . . . . . 13
⊢ (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 353 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑓‘suc 𝑐) ∈ V | 
| 354 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V | 
| 355 | 353, 354 | ifex 4575 | . . . . . . . . . . . . 13
⊢ if(suc
𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V | 
| 356 | 352, 32, 355 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (suc
𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 357 | 346, 356 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))) | 
| 358 | 329, 342,
357 | 3brtr4d 5174 | . . . . . . . . . 10
⊢ ((((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) | 
| 359 | 358 | ralrimiva 3145 | . . . . . . . . 9
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) | 
| 360 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (𝑓‘𝑝) ∈ V | 
| 361 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V | 
| 362 | 360, 361 | ifex 4575 | . . . . . . . . . . 11
⊢ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V | 
| 363 | 362, 32 | fnmpti 6710 | . . . . . . . . . 10
⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚) | 
| 364 | 46 | sucex 7827 | . . . . . . . . . . . 12
⊢ suc
(𝑛 +o 𝑚) ∈ V | 
| 365 | 364 | mptex 7244 | . . . . . . . . . . 11
⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V | 
| 366 |  | fneq1 6658 | . . . . . . . . . . . 12
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚))) | 
| 367 |  | fveq1 6904 | . . . . . . . . . . . . . 14
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘∅) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅)) | 
| 368 | 367 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘∅) = 𝑥 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥)) | 
| 369 |  | fveq1 6904 | . . . . . . . . . . . . . 14
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘(𝑛 +o 𝑚)) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚))) | 
| 370 | 369 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘(𝑛 +o 𝑚)) = 𝑦 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)) | 
| 371 | 368, 370 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦))) | 
| 372 |  | fveq1 6904 | . . . . . . . . . . . . . 14
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)) | 
| 373 |  | fveq1 6904 | . . . . . . . . . . . . . 14
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘suc 𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) | 
| 374 | 372, 373 | breq12d 5155 | . . . . . . . . . . . . 13
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))) | 
| 375 | 374 | ralbidv 3177 | . . . . . . . . . . . 12
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))) | 
| 376 | 366, 371,
375 | 3anbi123d 1437 | . . . . . . . . . . 11
⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚) ∧ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))) | 
| 377 | 365, 376 | spcev 3605 | . . . . . . . . . 10
⊢ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚) ∧ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 378 | 363, 377 | mp3an1 1449 | . . . . . . . . 9
⊢
(((((𝑝 ∈ suc
(𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 379 | 45, 123, 359, 378 | syl21anc 837 | . . . . . . . 8
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 380 |  | suceq 6449 | . . . . . . . . . . . 12
⊢ (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚)) | 
| 381 | 380 | fneq2d 6661 | . . . . . . . . . . 11
⊢ (𝑝 = (𝑛 +o 𝑚) → (ℎ Fn suc 𝑝 ↔ ℎ Fn suc (𝑛 +o 𝑚))) | 
| 382 |  | fveqeq2 6914 | . . . . . . . . . . . 12
⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ‘𝑝) = 𝑦 ↔ (ℎ‘(𝑛 +o 𝑚)) = 𝑦)) | 
| 383 | 382 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑝 = (𝑛 +o 𝑚) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ↔ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦))) | 
| 384 |  | raleq 3322 | . . . . . . . . . . 11
⊢ (𝑝 = (𝑛 +o 𝑚) → (∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 385 | 381, 383,
384 | 3anbi123d 1437 | . . . . . . . . . 10
⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ (ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))) | 
| 386 | 385 | exbidv 1920 | . . . . . . . . 9
⊢ (𝑝 = (𝑛 +o 𝑚) → (∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))) | 
| 387 | 386 | rspcev 3621 | . . . . . . . 8
⊢ (((𝑛 +o 𝑚) ∈ (ω ∖
1o) ∧ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 388 | 23, 379, 387 | syl2an2r 685 | . . . . . . 7
⊢ (((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 389 | 388 | ex 412 | . . . . . 6
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))) | 
| 390 | 389 | exlimdvv 1933 | . . . . 5
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ 𝑚
∈ (ω ∖ 1o)) → (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))) | 
| 391 | 390 | rexlimivv 3200 | . . . 4
⊢
(∃𝑛 ∈
(ω ∖ 1o)∃𝑚 ∈ (ω ∖
1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 392 | 391 | exlimiv 1929 | . . 3
⊢
(∃𝑧∃𝑛 ∈ (ω ∖
1o)∃𝑚
∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 393 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 394 |  | vex 3483 | . . . . 5
⊢ 𝑦 ∈ V | 
| 395 | 393, 394 | opelco 5881 | . . . 4
⊢
(〈𝑥, 𝑦〉 ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦)) | 
| 396 |  | reeanv 3228 | . . . . . 6
⊢
(∃𝑛 ∈
(ω ∖ 1o)∃𝑚 ∈ (ω ∖
1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖
1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 397 |  | eeanv 2350 | . . . . . . 7
⊢
(∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 398 | 397 | 2rexbii 3128 | . . . . . 6
⊢
(∃𝑛 ∈
(ω ∖ 1o)∃𝑚 ∈ (ω ∖
1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ ∃𝑛 ∈ (ω ∖
1o)∃𝑚
∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 399 |  | brttrcl 9754 | . . . . . . 7
⊢ (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) | 
| 400 |  | brttrcl 9754 | . . . . . . 7
⊢ (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖
1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) | 
| 401 | 399, 400 | anbi12i 628 | . . . . . 6
⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ (∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖
1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 402 | 396, 398,
401 | 3bitr4ri 304 | . . . . 5
⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ ∃𝑛 ∈ (ω ∖
1o)∃𝑚
∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 403 | 402 | exbii 1847 | . . . 4
⊢
(∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ ∃𝑧∃𝑛 ∈ (ω ∖
1o)∃𝑚
∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 404 | 395, 403 | bitri 275 | . . 3
⊢
(〈𝑥, 𝑦〉 ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧∃𝑛 ∈ (ω ∖
1o)∃𝑚
∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) | 
| 405 |  | df-br 5143 | . . . 4
⊢ (𝑥t++𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ t++𝑅) | 
| 406 |  | brttrcl 9754 | . . . 4
⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 407 | 405, 406 | bitr3i 277 | . . 3
⊢
(〈𝑥, 𝑦〉 ∈ t++𝑅 ↔ ∃𝑝 ∈ (ω ∖
1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) | 
| 408 | 392, 404,
407 | 3imtr4i 292 | . 2
⊢
(〈𝑥, 𝑦〉 ∈ (t++𝑅 ∘ t++𝑅) → 〈𝑥, 𝑦〉 ∈ t++𝑅) | 
| 409 | 1, 408 | relssi 5796 | 1
⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅 |