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

Theorem ttrcltr 9757
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 6125 . 2 Rel (t++𝑅 ∘ t++𝑅)
2 eldifi 4130 . . . . . . . . . 10 (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3 eldifi 4130 . . . . . . . . . 10 (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4 nnacl 8650 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
52, 3, 4syl2an 596 . . . . . . . . 9 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6 eldif 3960 . . . . . . . . . . . . 13 (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7 1on 8519 . . . . . . . . . . . . . . . 16 1o ∈ On
87onordi 6494 . . . . . . . . . . . . . . 15 Ord 1o
9 nnord 7896 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → Ord 𝑛)
10 ordtri1 6416 . . . . . . . . . . . . . . 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 8668 . . . . . . . . . . . 12 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
162, 3, 15syl2an 596 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
1714, 16sstrd 3993 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18 nnord 7896 . . . . . . . . . . . 12 ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
195, 18syl 17 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20 ordtri1 6416 . . . . . . . . . . 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 3961 . . . . . . . 8 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24 0elsuc 7856 . . . . . . . . . . . . 13 (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
2519, 24syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26 eleq1 2828 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27 fveq2 6905 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑓𝑝) = (𝑓‘∅))
28 eqeq2 2748 . . . . . . . . . . . . . . . 16 (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
2928riotabidv 7391 . . . . . . . . . . . . . . 15 (𝑝 = ∅ → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
3029fveq2d 6909 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
3126, 27, 30ifbieq12d 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
3533, 34ifex 4575 . . . . . . . . . . . . 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 7856 . . . . . . . . . . . . 13 (Ord 𝑛 → ∅ ∈ suc 𝑛)
4139, 40syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
4241iftrued 4532 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅))
4337, 42eqtrd 2776 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅))
44 simpl2l 1226 . . . . . . . . . 10 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘∅) = 𝑥)
4543, 44sylan9eq 2796 . . . . . . . . 9 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥)
46 ovex 7465 . . . . . . . . . . . . 13 (𝑛 +o 𝑚) ∈ V
4746sucid 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 𝑚)))
5150riotabidv 7391 . . . . . . . . . . . . . . 15 (𝑝 = (𝑛 +o 𝑚) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
5251fveq2d 6909 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
5348, 49, 52ifbieq12d 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
5654, 55ifex 4575 . . . . . . . . . . . . 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 8507 . . . . . . . . . . . . . . . . . 18 1o = suc ∅
6059difeq2i 4122 . . . . . . . . . . . . . . . . 17 (ω ∖ 1o) = (ω ∖ suc ∅)
6160eleq2i 2832 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62 peano1 7911 . . . . . . . . . . . . . . . . 17 ∅ ∈ ω
63 eldifsucnn 8703 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
6462, 63ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65 dif0 4377 . . . . . . . . . . . . . . . . 17 (ω ∖ ∅) = ω
6665rexeqi 3324 . . . . . . . . . . . . . . . 16 (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
6761, 64, 663bitri 297 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
6860eleq2i 2832 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69 eldifsucnn 8703 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
7062, 69ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
7165rexeqi 3324 . . . . . . . . . . . . . . . 16 (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
7268, 70, 713bitri 297 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
7367, 72anbi12i 628 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74 reeanv 3228 . . . . . . . . . . . . . 14 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
7573, 74bitr4i 278 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦))
76 peano2 7913 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77 nnaword1 8668 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
7876, 77sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
7976adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80 nnord 7896 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑥 ∈ ω → Ord suc 𝑥)
8179, 80syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82 nnacl 8650 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
8376, 82sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84 nnord 7896 . . . . . . . . . . . . . . . . . . . 20 ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
8583, 84syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86 ordsucsssuc 7844 . . . . . . . . . . . . . . . . . . 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 8645 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
9076, 89sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
9188, 90sseqtrrd 4020 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92 peano2 7913 . . . . . . . . . . . . . . . . . . 19 (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
9379, 92syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94 nnord 7896 . . . . . . . . . . . . . . . . . 18 (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96 peano2 7913 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97 nnacl 8650 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
9876, 96, 97syl2an 596 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99 nnord 7896 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
10098, 99syl 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 𝑥))
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 7441 . . . . . . . . . . . . . . . . 17 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105 suceq 6449 . . . . . . . . . . . . . . . . . 18 (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106105adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107104, 106eleq12d 2834 . . . . . . . . . . . . . . . 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 3200 . . . . . . . . . . . . 13 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
11175, 110sylbi 217 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112111iffalsed 4535 . . . . . . . . . . 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 8667 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118114, 115, 116, 117syl3anc 1372 . . . . . . . . . . . . 13 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119113, 118riota5 7418 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120119fveq2d 6909 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔𝑚))
12158, 112, 1203eqtrd 2780 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔𝑚))
122 simpr2r 1233 . . . . . . . . . 10 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔𝑚) = 𝑦)
123121, 122sylan9eq 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 𝑐)
127126fveq2d 6909 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128125, 127breq12d 5155 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑐 → ((𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓𝑐)𝑅(𝑓‘suc 𝑐)))
129128rspcv 3617 . . . . . . . . . . . . . . 15 (𝑐𝑛 → (∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓𝑐)𝑅(𝑓‘suc 𝑐)))
130124, 129mpan9 506 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → (𝑓𝑐)𝑅(𝑓‘suc 𝑐))
131 elelsuc 6456 . . . . . . . . . . . . . . . 16 (𝑐𝑛𝑐 ∈ suc 𝑛)
132131adantl 481 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → 𝑐 ∈ suc 𝑛)
133132iftrued 4532 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓𝑐))
134 ordsucelsuc 7843 . . . . . . . . . . . . . . . . . 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 4532 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139130, 133, 1383brtr4d 5174 . . . . . . . . . . . . 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 7899 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144143ancoms 458 . . . . . . . . . . . . . . . . . . 19 (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145142, 144sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146 nnord 7896 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ω → Ord 𝑐)
147145, 146syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148 ordtri3or 6415 . . . . . . . . . . . . . . . . 17 ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛𝑐𝑛 = 𝑐𝑐𝑛))
149141, 147, 148syl2an2r 685 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛𝑐𝑛 = 𝑐𝑐𝑛))
150 3orel3 1487 . . . . . . . . . . . . . . . 16 𝑐𝑛 → ((𝑛𝑐𝑛 = 𝑐𝑐𝑛) → (𝑛𝑐𝑛 = 𝑐)))
151149, 150syl5com 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 𝑞) = 𝑐))
154153fveq2d 6909 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155152, 154breq12d 5155 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156 simprr3 1223 . . . . . . . . . . . . . . . . . . . . 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 6399 . . . . . . . . . . . . . . . . . . . . . . . . 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 8676 . . . . . . . . . . . . . . . . . . . . . . . . 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 7440 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168167eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169168cbvrexvw 3237 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170166, 169sylib 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 𝑚))
173171, 172eqeltrd 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 𝑝) = 𝑐)) → 𝑝 ∈ ω)
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 8658 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180174, 176, 178, 179syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 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 3172 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝𝑚 (𝑛 +o 𝑝) = 𝑐)
183 elnn 7899 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑚𝑚 ∈ ω) → 𝑝 ∈ ω)
184183ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ ω ∧ 𝑝𝑚) → 𝑝 ∈ ω)
185175, 184sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → 𝑝 ∈ ω)
186 nnasmo 8702 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187177, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188 reu5 3381 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7414 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
192185, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
193 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
194192, 193bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ((𝑛 +o 𝑝) = 𝑐𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195194rexbidva 3176 . . . . . . . . . . . . . . . . . . . . 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 3232 . . . . . . . . . . . . . . . . . . . 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 3483 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ V
202147adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → Ord 𝑐)
203 ordelsuc 7841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛𝑐 ↔ suc 𝑛𝑐))
204201, 202, 203sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ suc 𝑛𝑐))
205 peano2 7913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
20638, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207 nnord 7896 . . . . . . . . . . . . . . . . . . . . . . . . 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 6416 . . . . . . . . . . . . . . . . . . . . . 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 4535 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216 riotacl 7406 . . . . . . . . . . . . . . . . . . . . . . 23 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217189, 216syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218 nnasuc 8645 . . . . . . . . . . . . . . . . . . . . . 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 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
224222, 223, 221nfov 7462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑞(𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225224nfeq1 2920 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞(𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226 oveq2 7440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227226eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228221, 225, 227riota2f 7413 . . . . . . . . . . . . . . . . . . . . . . . 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 6449 . . . . . . . . . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
234 peano2 7913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235217, 234syl 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 𝑝))
238177, 237sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239 oveq2 7440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240239eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244243eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245244rexbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
246242, 245syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → ((𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
247246rexlimdva 3154 . . . . . . . . . . . . . . . . . . . . . . 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 8702 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250177, 249syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251 reu5 3381 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252248, 250, 251sylanbrc 583 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253221nfsuc 6455 . . . . . . . . . . . . . . . . . . . . . 22 𝑞 suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254222, 223, 253nfov 7462 . . . . . . . . . . . . . . . . . . . . . . 23 𝑞(𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255254nfeq1 2920 . . . . . . . . . . . . . . . . . . . . . 22 𝑞(𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256 oveq2 7440 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257256eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258253, 255, 257riota2f 7413 . . . . . . . . . . . . . . . . . . . . 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 6909 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262199, 215, 2613brtr4d 5174 . . . . . . . . . . . . . . . . 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 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → (𝑔𝑏) = (𝑔‘∅))
265 suceq 6449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = ∅ → suc 𝑏 = suc ∅)
266265, 59eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = ∅ → suc 𝑏 = 1o)
267266fveq2d 6909 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268264, 267breq12d 5155 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ∅ → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269 eldif 3960 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270 nnord 7896 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ω → Ord 𝑚)
271 ordtri1 6416 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4022 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277 0ex 5306 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
278113, 270syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279 ordelsuc 7841 . . . . . . . . . . . . . . . . . . . . . . 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 1227 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓𝑛) = 𝑧)
285 simpr2l 1232 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘∅) = 𝑧)
286284, 285eqtr4d 2779 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓𝑛) = (𝑔‘∅))
287286adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓𝑛) = (𝑔‘∅))
288 nnon 7894 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → 𝑛 ∈ On)
28938, 288syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290 oa1suc 8570 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291289, 290syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292 1onn 8679 . . . . . . . . . . . . . . . . . . . . . . 23 1o ∈ ω
293 oveq2 7440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294293eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8702 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
29838, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299 reu5 3381 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300296, 298, 299sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301294riota2 7414 . . . . . . . . . . . . . . . . . . . . . . 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 6909 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306283, 287, 3053brtr4d 5174 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓𝑛)𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307201sucid 6465 . . . . . . . . . . . . . . . . . . . . 21 𝑛 ∈ suc 𝑛
308307iftruei 4531 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 ∈ suc 𝑛, (𝑓𝑛), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓𝑛)
309 eleq1 2828 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛𝑐 ∈ suc 𝑛))
310 fveq2 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → (𝑓𝑛) = (𝑓𝑐))
311309, 310ifbieq1d 4549 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓𝑛), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312308, 311eqtr3id 2790 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑐 → (𝑓𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313 suceq 6449 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314313eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315314riotabidv 7391 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316315fveq2d 6909 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317312, 316breq12d 5155 . . . . . . . . . . . . . . . . . 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 4535 . . . . . . . . . . . . 13 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328322, 327breqtrrd 5170 . . . . . . . . . . . 12 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329140, 328pm2.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 𝑚))
331330adantl 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 𝑞) = 𝑐))
335334riotabidv 7391 . . . . . . . . . . . . . . 15 (𝑝 = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336335fveq2d 6909 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337332, 333, 336ifbieq12d 4553 . . . . . . . . . . . . 13 (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338 fvex 6918 . . . . . . . . . . . . . 14 (𝑓𝑐) ∈ V
339 fvex 6918 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340338, 339ifex 4575 . . . . . . . . . . . . 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 7843 . . . . . . . . . . . . . . 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 2828 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348 fveq2 6905 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑓𝑝) = (𝑓‘suc 𝑐))
349 eqeq2 2748 . . . . . . . . . . . . . . . 16 (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350349riotabidv 7391 . . . . . . . . . . . . . . 15 (𝑝 = suc 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351350fveq2d 6909 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352347, 348, 351ifbieq12d 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
355353, 354ifex 4575 . . . . . . . . . . . . 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 5174 . . . . . . . . . 10 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
359358ralrimiva 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
362360, 361ifex 4575 . . . . . . . . . . 11 if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363362, 32fnmpti 6710 . . . . . . . . . 10 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
36446sucex 7827 . . . . . . . . . . . 12 suc (𝑛 +o 𝑚) ∈ V
365364mptex 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 𝑞) = 𝑝))))‘∅))
368367eqeq1d 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 𝑚)))
370369eqeq1d 2738 . . . . . . . . . . . . 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 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 𝑐))
374372, 373breq12d 5155 . . . . . . . . . . . . 13 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((𝑐)𝑅(‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
375374ralbidv 3177 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
376366, 371, 3753anbi123d 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 𝑐))))
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 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 𝑐)))
37945, 123, 359, 378syl21anc 837 . . . . . . . 8 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐)))
380 suceq 6449 . . . . . . . . . . . 12 (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381380fneq2d 6661 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → ( Fn suc 𝑝 Fn suc (𝑛 +o 𝑚)))
382 fveqeq2 6914 . . . . . . . . . . . 12 (𝑝 = (𝑛 +o 𝑚) → ((𝑝) = 𝑦 ↔ (‘(𝑛 +o 𝑚)) = 𝑦))
383382anbi2d 630 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → (((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ↔ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦)))
384 raleq 3322 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → (∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐)))
385381, 383, 3843anbi123d 1437 . . . . . . . . . 10 (𝑝 = (𝑛 +o 𝑚) → (( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)) ↔ ( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))))
386385exbidv 1920 . . . . . . . . 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 1933 . . . . 5 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐))))
391390rexlimivv 3200 . . . 4 (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
392391exlimiv 1929 . . 3 (∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
393 vex 3483 . . . . 5 𝑥 ∈ V
394 vex 3483 . . . . 5 𝑦 ∈ V
395393, 394opelco 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 𝑏))))
3983972rexbii 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 𝑏)))
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 1847 . . . 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 5143 . . . 4 (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406 brttrcl 9754 . . . 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 5796 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 1539  wex 1778  wcel 2107  wral 3060  wrex 3069  ∃!wreu 3377  ∃*wrmo 3378  Vcvv 3479  cdif 3947  wss 3950  c0 4332  ifcif 4524  cop 4631   class class class wbr 5142  cmpt 5224  ccom 5688  Ord word 6382  Oncon0 6383  suc csuc 6385   Fn wfn 6555  cfv 6560  crio 7388  (class class class)co 7432  ωcom 7888  1oc1o 8500   +o coa 8504  t++cttrcl 9748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-oadd 8511  df-ttrcl 9749
This theorem is referenced by:  ttrclco  9759  cottrcl  9760  dfttrcl2  9765  frmin  9790  frrlem16  9799
  Copyright terms: Public domain W3C validator