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

Theorem ttrcltr 9753
Description: The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024.)
Assertion
Ref Expression
ttrcltr (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅

Proof of Theorem ttrcltr
Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 𝑛 𝑚 𝑝 𝑞 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 6128 . 2 Rel (t++𝑅 ∘ t++𝑅)
2 eldifi 4140 . . . . . . . . . 10 (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3 eldifi 4140 . . . . . . . . . 10 (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4 nnacl 8647 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
52, 3, 4syl2an 596 . . . . . . . . 9 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6 eldif 3972 . . . . . . . . . . . . 13 (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7 1on 8516 . . . . . . . . . . . . . . . 16 1o ∈ On
87onordi 6496 . . . . . . . . . . . . . . 15 Ord 1o
9 nnord 7894 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → Ord 𝑛)
10 ordtri1 6418 . . . . . . . . . . . . . . 15 ((Ord 1o ∧ Ord 𝑛) → (1o𝑛 ↔ ¬ 𝑛 ∈ 1o))
118, 9, 10sylancr 587 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (1o𝑛 ↔ ¬ 𝑛 ∈ 1o))
1211biimpar 477 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o) → 1o𝑛)
136, 12sylbi 217 . . . . . . . . . . . 12 (𝑛 ∈ (ω ∖ 1o) → 1o𝑛)
1413adantr 480 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o𝑛)
15 nnaword1 8665 . . . . . . . . . . . 12 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
162, 3, 15syl2an 596 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
1714, 16sstrd 4005 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18 nnord 7894 . . . . . . . . . . . 12 ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
195, 18syl 17 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20 ordtri1 6418 . . . . . . . . . . 11 ((Ord 1o ∧ Ord (𝑛 +o 𝑚)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
218, 19, 20sylancr 587 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
2217, 21mpbid 232 . . . . . . . . 9 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o)
235, 22eldifd 3973 . . . . . . . 8 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24 0elsuc 7854 . . . . . . . . . . . . 13 (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
2519, 24syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26 eleq1 2826 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27 fveq2 6906 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑓𝑝) = (𝑓‘∅))
28 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
2928riotabidv 7389 . . . . . . . . . . . . . . 15 (𝑝 = ∅ → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
3029fveq2d 6910 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
3126, 27, 30ifbieq12d 4558 . . . . . . . . . . . . 13 (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
32 eqid 2734 . . . . . . . . . . . . 13 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))
33 fvex 6919 . . . . . . . . . . . . . 14 (𝑓‘∅) ∈ V
34 fvex 6919 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈ V
3533, 34ifex 4580 . . . . . . . . . . . . 13 if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V
3631, 32, 35fvmpt 7015 . . . . . . . . . . . 12 (∅ ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
3725, 36syl 17 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
382adantr 480 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ ω)
3938, 9syl 17 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑛)
40 0elsuc 7854 . . . . . . . . . . . . 13 (Ord 𝑛 → ∅ ∈ suc 𝑛)
4139, 40syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
4241iftrued 4538 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅))
4337, 42eqtrd 2774 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅))
44 simpl2l 1225 . . . . . . . . . 10 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘∅) = 𝑥)
4543, 44sylan9eq 2794 . . . . . . . . 9 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥)
46 ovex 7463 . . . . . . . . . . . . 13 (𝑛 +o 𝑚) ∈ V
4746sucid 6467 . . . . . . . . . . . 12 (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚)
48 eleq1 2826 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛))
49 fveq2 6906 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑓𝑝) = (𝑓‘(𝑛 +o 𝑚)))
50 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
5150riotabidv 7389 . . . . . . . . . . . . . . 15 (𝑝 = (𝑛 +o 𝑚) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
5251fveq2d 6910 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
5348, 49, 52ifbieq12d 4558 . . . . . . . . . . . . 13 (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
54 fvex 6919 . . . . . . . . . . . . . 14 (𝑓‘(𝑛 +o 𝑚)) ∈ V
55 fvex 6919 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V
5654, 55ifex 4580 . . . . . . . . . . . . 13 if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V
5753, 32, 56fvmpt 7015 . . . . . . . . . . . 12 ((𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
5847, 57mp1i 13 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
59 df-1o 8504 . . . . . . . . . . . . . . . . . 18 1o = suc ∅
6059difeq2i 4132 . . . . . . . . . . . . . . . . 17 (ω ∖ 1o) = (ω ∖ suc ∅)
6160eleq2i 2830 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62 peano1 7910 . . . . . . . . . . . . . . . . 17 ∅ ∈ ω
63 eldifsucnn 8700 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
6462, 63ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65 dif0 4383 . . . . . . . . . . . . . . . . 17 (ω ∖ ∅) = ω
6665rexeqi 3322 . . . . . . . . . . . . . . . 16 (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
6761, 64, 663bitri 297 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
6860eleq2i 2830 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69 eldifsucnn 8700 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
7062, 69ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
7165rexeqi 3322 . . . . . . . . . . . . . . . 16 (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
7268, 70, 713bitri 297 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
7367, 72anbi12i 628 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74 reeanv 3226 . . . . . . . . . . . . . 14 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
7573, 74bitr4i 278 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦))
76 peano2 7912 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77 nnaword1 8665 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
7876, 77sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
7976adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80 nnord 7894 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑥 ∈ ω → Ord suc 𝑥)
8179, 80syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82 nnacl 8647 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
8376, 82sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84 nnord 7894 . . . . . . . . . . . . . . . . . . . 20 ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
8583, 84syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86 ordsucsssuc 7842 . . . . . . . . . . . . . . . . . . 19 ((Ord suc 𝑥 ∧ Ord (suc 𝑥 +o 𝑦)) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
8781, 85, 86syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
8878, 87mpbid 232 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))
89 nnasuc 8642 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
9076, 89sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
9188, 90sseqtrrd 4036 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92 peano2 7912 . . . . . . . . . . . . . . . . . . 19 (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
9379, 92syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94 nnord 7894 . . . . . . . . . . . . . . . . . 18 (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96 peano2 7912 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97 nnacl 8647 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
9876, 96, 97syl2an 596 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99 nnord 7894 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o suc 𝑦))
101 ordtri1 6418 . . . . . . . . . . . . . . . . 17 ((Ord suc suc 𝑥 ∧ Ord (suc 𝑥 +o suc 𝑦)) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
10295, 100, 101syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
10391, 102mpbid 232 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)
104 oveq12 7439 . . . . . . . . . . . . . . . . 17 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105 suceq 6451 . . . . . . . . . . . . . . . . . 18 (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106105adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107104, 106eleq12d 2832 . . . . . . . . . . . . . . . 16 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → ((𝑛 +o 𝑚) ∈ suc 𝑛 ↔ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
108107notbid 318 . . . . . . . . . . . . . . 15 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → (¬ (𝑛 +o 𝑚) ∈ suc 𝑛 ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
109103, 108syl5ibrcom 247 . . . . . . . . . . . . . 14 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛))
110109rexlimivv 3198 . . . . . . . . . . . . 13 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
11175, 110sylbi 217 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112111iffalsed 4541 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
1133adantl 481 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑚 ∈ ω)
11438adantr 480 . . . . . . . . . . . . . 14 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑛 ∈ ω)
115 simpr 484 . . . . . . . . . . . . . 14 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑞 ∈ ω)
116113adantr 480 . . . . . . . . . . . . . 14 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑚 ∈ ω)
117 nnacan 8664 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118114, 115, 116, 117syl3anc 1370 . . . . . . . . . . . . 13 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119113, 118riota5 7416 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120119fveq2d 6910 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔𝑚))
12158, 112, 1203eqtrd 2778 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔𝑚))
122 simpr2r 1232 . . . . . . . . . 10 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔𝑚) = 𝑦)
123121, 122sylan9eq 2794 . . . . . . . . 9 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)
124 simprl3 1219 . . . . . . . . . . . . . . 15 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎))
125 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → (𝑓𝑎) = (𝑓𝑐))
126 suceq 6451 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
127126fveq2d 6910 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128125, 127breq12d 5160 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑐 → ((𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓𝑐)𝑅(𝑓‘suc 𝑐)))
129128rspcv 3617 . . . . . . . . . . . . . . 15 (𝑐𝑛 → (∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓𝑐)𝑅(𝑓‘suc 𝑐)))
130124, 129mpan9 506 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → (𝑓𝑐)𝑅(𝑓‘suc 𝑐))
131 elelsuc 6458 . . . . . . . . . . . . . . . 16 (𝑐𝑛𝑐 ∈ suc 𝑛)
132131adantl 481 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → 𝑐 ∈ suc 𝑛)
133132iftrued 4538 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓𝑐))
134 ordsucelsuc 7841 . . . . . . . . . . . . . . . . . 18 (Ord 𝑛 → (𝑐𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
13539, 134syl 17 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
136135adantr 480 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
137136biimpa 476 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → suc 𝑐 ∈ suc 𝑛)
138137iftrued 4538 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139130, 133, 1383brtr4d 5179 . . . . . . . . . . . . 13 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
140139adantlr 715 . . . . . . . . . . . 12 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
14139adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord 𝑛)
1425adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 +o 𝑚) ∈ ω)
143 elnn 7897 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144143ancoms 458 . . . . . . . . . . . . . . . . . . 19 (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145142, 144sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146 nnord 7894 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ω → Ord 𝑐)
147145, 146syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148 ordtri3or 6417 . . . . . . . . . . . . . . . . 17 ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛𝑐𝑛 = 𝑐𝑐𝑛))
149141, 147, 148syl2an2r 685 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛𝑐𝑛 = 𝑐𝑐𝑛))
150 3orel3 1484 . . . . . . . . . . . . . . . 16 𝑐𝑛 → ((𝑛𝑐𝑛 = 𝑐𝑐𝑛) → (𝑛𝑐𝑛 = 𝑐)))
151149, 150syl5com 31 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐𝑛 → (𝑛𝑐𝑛 = 𝑐)))
152 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔𝑏) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
153 suceq 6451 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
154153fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155152, 154breq12d 5160 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156 simprr3 1222 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))
157156adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))
158157adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))
159 ordelss 6401 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord 𝑐𝑛𝑐) → 𝑛𝑐)
160147, 159sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑛𝑐)
16138adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → 𝑛 ∈ ω)
162161adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑛 ∈ ω)
163145adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑐 ∈ ω)
164 nnawordex 8673 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
165162, 163, 164syl2an2r 685 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
166160, 165mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
167 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168167eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169168cbvrexvw 3235 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170166, 169sylib 218 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
171 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐)
172 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑐 ∈ (𝑛 +o 𝑚))
173171, 172eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))
174 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω)
1753ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑚 ∈ ω)
176175adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑚 ∈ ω)
177162adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑛 ∈ ω)
178177adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑛 ∈ ω)
179 nnaord 8655 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180174, 176, 178, 179syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑝𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
181173, 180mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝𝑚)
182170, 181, 171reximssdv 3170 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝𝑚 (𝑛 +o 𝑝) = 𝑐)
183 elnn 7897 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑚𝑚 ∈ ω) → 𝑝 ∈ ω)
184183ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ ω ∧ 𝑝𝑚) → 𝑝 ∈ ω)
185175, 184sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → 𝑝 ∈ ω)
186 nnasmo 8699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187177, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188 reu5 3379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
189166, 187, 188sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
190189adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
191168riota2 7412 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
192185, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
193 eqcom 2741 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
194192, 193bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ((𝑛 +o 𝑝) = 𝑐𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195194rexbidva 3174 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (∃𝑝𝑚 (𝑛 +o 𝑝) = 𝑐 ↔ ∃𝑝𝑚 𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
196182, 195mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝𝑚 𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
197 risset 3230 . . . . . . . . . . . . . . . . . . . 20 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝𝑚 𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
198196, 197sylibr 234 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚)
199155, 158, 198rspcdva 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 3481 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ V
202147adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → Ord 𝑐)
203 ordelsuc 7839 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛𝑐 ↔ suc 𝑛𝑐))
204201, 202, 203sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ suc 𝑛𝑐))
205 peano2 7912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
20638, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207 nnord 7894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (suc 𝑛 ∈ ω → Ord suc 𝑛)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord suc 𝑛)
209208adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord suc 𝑛)
210209adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord suc 𝑛)
211 ordtri1 6418 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord suc 𝑛 ∧ Ord 𝑐) → (suc 𝑛𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
212210, 202, 211syl2an2r 685 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (suc 𝑛𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
213204, 212bitrd 279 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
214200, 213mpbid 232 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ¬ 𝑐 ∈ suc 𝑛)
215214iffalsed 4541 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216 riotacl 7404 . . . . . . . . . . . . . . . . . . . . . . 23 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217189, 216syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218 nnasuc 8642 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
219162, 217, 218syl2an2r 685 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
220 eqidd 2735 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
221 nfriota1 7394 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
222 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞𝑛
223 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞 +o
224222, 223, 221nfov 7460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑞(𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225224nfeq1 2918 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞(𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227226eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228221, 225, 227riota2f 7411 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
229217, 189, 228syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ((𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
230220, 229mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐)
231 suceq 6451 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 → suc (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → suc (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
233219, 232eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
234 peano2 7912 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235217, 234syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
236 peano2 7912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ω → suc 𝑝 ∈ ω)
237 nnasuc 8642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
238177, 237sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240239eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)))
241240rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((suc 𝑝 ∈ ω ∧ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
242236, 238, 241syl2an2 686 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
243 suceq 6451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244243eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245244rexbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
246242, 245syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → ((𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
247246rexlimdva 3152 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
248170, 247mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
249 nnasmo 8699 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250177, 249syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251 reu5 3379 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252248, 250, 251sylanbrc 583 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253221nfsuc 6457 . . . . . . . . . . . . . . . . . . . . . 22 𝑞 suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254222, 223, 253nfov 7460 . . . . . . . . . . . . . . . . . . . . . . 23 𝑞(𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255254nfeq1 2918 . . . . . . . . . . . . . . . . . . . . . 22 𝑞(𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257256eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258253, 255, 257riota2f 7411 . . . . . . . . . . . . . . . . . . . . 21 ((suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) → ((𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
259235, 252, 258syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ((𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
260233, 259mpbid 232 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
261260fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262199, 215, 2613brtr4d 5179 . . . . . . . . . . . . . . . . 17 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
263262ex 412 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
264 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → (𝑔𝑏) = (𝑔‘∅))
265 suceq 6451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = ∅ → suc 𝑏 = suc ∅)
266265, 59eqtr4di 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = ∅ → suc 𝑏 = 1o)
267266fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268264, 267breq12d 5160 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ∅ → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269 eldif 3972 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270 nnord 7894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ω → Ord 𝑚)
271 ordtri1 6418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 1o ∧ Ord 𝑚) → (1o𝑚 ↔ ¬ 𝑚 ∈ 1o))
2728, 270, 271sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ ω → (1o𝑚 ↔ ¬ 𝑚 ∈ 1o))
273272biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o) → 1o𝑚)
274269, 273sylbi 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (ω ∖ 1o) → 1o𝑚)
275274adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o𝑚)
27659, 275eqsstrrid 4044 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277 0ex 5312 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
278113, 270syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279 ordelsuc 7839 . . . . . . . . . . . . . . . . . . . . . . 23 ((∅ ∈ V ∧ Ord 𝑚) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
280277, 278, 279sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
281276, 280mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ 𝑚)
282281adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∅ ∈ 𝑚)
283268, 156, 282rspcdva 3622 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘∅)𝑅(𝑔‘1o))
284 simpl2r 1226 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓𝑛) = 𝑧)
285 simpr2l 1231 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘∅) = 𝑧)
286284, 285eqtr4d 2777 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓𝑛) = (𝑔‘∅))
287286adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓𝑛) = (𝑔‘∅))
288 nnon 7892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → 𝑛 ∈ On)
28938, 288syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290 oa1suc 8567 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291289, 290syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292 1onn 8676 . . . . . . . . . . . . . . . . . . . . . . 23 1o ∈ ω
293 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294293eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛))
295294rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
296292, 291, 295sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
297 nnasmo 8699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
29838, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299 reu5 3379 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300296, 298, 299sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301294riota2 7412 . . . . . . . . . . . . . . . . . . . . . . 23 ((1o ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) → ((𝑛 +o 1o) = suc 𝑛 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
302292, 300, 301sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑛 +o 1o) = suc 𝑛 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
303291, 302mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
304303adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
305304fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306283, 287, 3053brtr4d 5179 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓𝑛)𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307201sucid 6467 . . . . . . . . . . . . . . . . . . . . 21 𝑛 ∈ suc 𝑛
308307iftruei 4537 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 ∈ suc 𝑛, (𝑓𝑛), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓𝑛)
309 eleq1 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛𝑐 ∈ suc 𝑛))
310 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → (𝑓𝑛) = (𝑓𝑐))
311309, 310ifbieq1d 4554 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓𝑛), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312308, 311eqtr3id 2788 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑐 → (𝑓𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313 suceq 6451 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314313eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315314riotabidv 7389 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316315fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317312, 316breq12d 5160 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑐 → ((𝑓𝑛)𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) ↔ if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
318306, 317syl5ibcom 245 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
319318adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
320263, 319jaod 859 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑛𝑐𝑛 = 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
321151, 320syld 47 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐𝑛 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
322321imp 406 . . . . . . . . . . . . 13 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
323135notbid 318 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (¬ 𝑐𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
324323adantr 480 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (¬ 𝑐𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
325324adantr 480 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
326325biimpa 476 . . . . . . . . . . . . . 14 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → ¬ suc 𝑐 ∈ suc 𝑛)
327326iffalsed 4541 . . . . . . . . . . . . 13 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328322, 327breqtrrd 5175 . . . . . . . . . . . 12 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329140, 328pm2.61dan 813 . . . . . . . . . . 11 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
330 elelsuc 6458 . . . . . . . . . . . . 13 (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚))
331330adantl 481 . . . . . . . . . . . 12 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚))
332 eleq1 2826 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛𝑐 ∈ suc 𝑛))
333 fveq2 6906 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑓𝑝) = (𝑓𝑐))
334 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐))
335334riotabidv 7389 . . . . . . . . . . . . . . 15 (𝑝 = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336335fveq2d 6910 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337332, 333, 336ifbieq12d 4558 . . . . . . . . . . . . 13 (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338 fvex 6919 . . . . . . . . . . . . . 14 (𝑓𝑐) ∈ V
339 fvex 6919 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340338, 339ifex 4580 . . . . . . . . . . . . 13 if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V
341337, 32, 340fvmpt 7015 . . . . . . . . . . . 12 (𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
342331, 341syl 17 . . . . . . . . . . 11 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
343 ordsucelsuc 7841 . . . . . . . . . . . . . . 15 (Ord (𝑛 +o 𝑚) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
34419, 343syl 17 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
345344adantr 480 . . . . . . . . . . . . 13 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
346345biimpa 476 . . . . . . . . . . . 12 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → suc 𝑐 ∈ suc (𝑛 +o 𝑚))
347 eleq1 2826 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348 fveq2 6906 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑓𝑝) = (𝑓‘suc 𝑐))
349 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350349riotabidv 7389 . . . . . . . . . . . . . . 15 (𝑝 = suc 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351350fveq2d 6910 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352347, 348, 351ifbieq12d 4558 . . . . . . . . . . . . 13 (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
353 fvex 6919 . . . . . . . . . . . . . 14 (𝑓‘suc 𝑐) ∈ V
354 fvex 6919 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V
355353, 354ifex 4580 . . . . . . . . . . . . 13 if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V
356352, 32, 355fvmpt 7015 . . . . . . . . . . . 12 (suc 𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
357346, 356syl 17 . . . . . . . . . . 11 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
358329, 342, 3573brtr4d 5179 . . . . . . . . . 10 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
359358ralrimiva 3143 . . . . . . . . 9 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
360 fvex 6919 . . . . . . . . . . . 12 (𝑓𝑝) ∈ V
361 fvex 6919 . . . . . . . . . . . 12 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V
362360, 361ifex 4580 . . . . . . . . . . 11 if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363362, 32fnmpti 6711 . . . . . . . . . 10 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
36446sucex 7825 . . . . . . . . . . . 12 suc (𝑛 +o 𝑚) ∈ V
365364mptex 7242 . . . . . . . . . . 11 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V
366 fneq1 6659 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ( Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)))
367 fveq1 6905 . . . . . . . . . . . . . 14 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (‘∅) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅))
368367eqeq1d 2736 . . . . . . . . . . . . 13 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((‘∅) = 𝑥 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥))
369 fveq1 6905 . . . . . . . . . . . . . 14 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (‘(𝑛 +o 𝑚)) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)))
370369eqeq1d 2736 . . . . . . . . . . . . 13 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((‘(𝑛 +o 𝑚)) = 𝑦 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦))
371368, 370anbi12d 632 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)))
372 fveq1 6905 . . . . . . . . . . . . . 14 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐))
373 fveq1 6905 . . . . . . . . . . . . . 14 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (‘suc 𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
374372, 373breq12d 5160 . . . . . . . . . . . . 13 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((𝑐)𝑅(‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
375374ralbidv 3175 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
376366, 371, 3753anbi123d 1435 . . . . . . . . . . 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 𝑐))))
377365, 376spcev 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 𝑐)))
378363, 377mp3an1 1447 . . . . . . . . 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 𝑐)))
37945, 123, 359, 378syl21anc 838 . . . . . . . 8 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐)))
380 suceq 6451 . . . . . . . . . . . 12 (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381380fneq2d 6662 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → ( Fn suc 𝑝 Fn suc (𝑛 +o 𝑚)))
382 fveqeq2 6915 . . . . . . . . . . . 12 (𝑝 = (𝑛 +o 𝑚) → ((𝑝) = 𝑦 ↔ (‘(𝑛 +o 𝑚)) = 𝑦))
383382anbi2d 630 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → (((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ↔ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦)))
384 raleq 3320 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → (∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐)))
385381, 383, 3843anbi123d 1435 . . . . . . . . . 10 (𝑝 = (𝑛 +o 𝑚) → (( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)) ↔ ( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))))
386385exbidv 1918 . . . . . . . . 9 (𝑝 = (𝑛 +o 𝑚) → (∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)) ↔ ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))))
387386rspcev 3621 . . . . . . . 8 (((𝑛 +o 𝑚) ∈ (ω ∖ 1o) ∧ ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
38823, 379, 387syl2an2r 685 . . . . . . 7 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
389388ex 412 . . . . . 6 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐))))
390389exlimdvv 1931 . . . . 5 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐))))
391390rexlimivv 3198 . . . 4 (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
392391exlimiv 1927 . . 3 (∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
393 vex 3481 . . . . 5 𝑥 ∈ V
394 vex 3481 . . . . 5 𝑦 ∈ V
395393, 394opelco 5884 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧𝑧t++𝑅𝑦))
396 reeanv 3226 . . . . . 6 (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
397 eeanv 2349 . . . . . . 7 (∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
3983972rexbii 3126 . . . . . 6 (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
399 brttrcl 9750 . . . . . . 7 (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
400 brttrcl 9750 . . . . . . 7 (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
401399, 400anbi12i 628 . . . . . 6 ((𝑥t++𝑅𝑧𝑧t++𝑅𝑦) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
402396, 398, 4013bitr4ri 304 . . . . 5 ((𝑥t++𝑅𝑧𝑧t++𝑅𝑦) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
403402exbii 1844 . . . 4 (∃𝑧(𝑥t++𝑅𝑧𝑧t++𝑅𝑦) ↔ ∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
404395, 403bitri 275 . . 3 (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
405 df-br 5148 . . . 4 (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406 brttrcl 9750 . . . 4 (𝑥t++𝑅𝑦 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
407405, 406bitr3i 277 . . 3 (⟨𝑥, 𝑦⟩ ∈ t++𝑅 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
408392, 404, 4073imtr4i 292 . 2 (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
4091, 408relssi 5799 1 (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wral 3058  wrex 3067  ∃!wreu 3375  ∃*wrmo 3376  Vcvv 3477  cdif 3959  wss 3962  c0 4338  ifcif 4530  cop 4636   class class class wbr 5147  cmpt 5230  ccom 5692  Ord word 6384  Oncon0 6385  suc csuc 6387   Fn wfn 6557  cfv 6562  crio 7386  (class class class)co 7430  ωcom 7886  1oc1o 8497   +o coa 8501  t++cttrcl 9744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-ttrcl 9745
This theorem is referenced by:  ttrclco  9755  cottrcl  9756  dfttrcl2  9761  frmin  9786  frrlem16  9795
  Copyright terms: Public domain W3C validator