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

Theorem ttrcltr 9652
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 6060 . 2 Rel (t++𝑅 ∘ t++𝑅)
2 eldifi 4086 . . . . . . . . . 10 (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3 eldifi 4086 . . . . . . . . . 10 (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4 nnacl 8558 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
52, 3, 4syl2an 596 . . . . . . . . 9 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6 eldif 3920 . . . . . . . . . . . . 13 (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7 1on 8424 . . . . . . . . . . . . . . . 16 1o ∈ On
87onordi 6428 . . . . . . . . . . . . . . 15 Ord 1o
9 nnord 7810 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → Ord 𝑛)
10 ordtri1 6350 . . . . . . . . . . . . . . 15 ((Ord 1o ∧ Ord 𝑛) → (1o𝑛 ↔ ¬ 𝑛 ∈ 1o))
118, 9, 10sylancr 587 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (1o𝑛 ↔ ¬ 𝑛 ∈ 1o))
1211biimpar 478 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o) → 1o𝑛)
136, 12sylbi 216 . . . . . . . . . . . 12 (𝑛 ∈ (ω ∖ 1o) → 1o𝑛)
1413adantr 481 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o𝑛)
15 nnaword1 8576 . . . . . . . . . . . 12 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
162, 3, 15syl2an 596 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
1714, 16sstrd 3954 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18 nnord 7810 . . . . . . . . . . . 12 ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
195, 18syl 17 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20 ordtri1 6350 . . . . . . . . . . 11 ((Ord 1o ∧ Ord (𝑛 +o 𝑚)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
218, 19, 20sylancr 587 . . . . . . . . . 10 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
2217, 21mpbid 231 . . . . . . . . 9 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o)
235, 22eldifd 3921 . . . . . . . 8 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24 0elsuc 7770 . . . . . . . . . . . . 13 (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
2519, 24syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26 eleq1 2825 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27 fveq2 6842 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑓𝑝) = (𝑓‘∅))
28 eqeq2 2748 . . . . . . . . . . . . . . . 16 (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
2928riotabidv 7315 . . . . . . . . . . . . . . 15 (𝑝 = ∅ → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
3029fveq2d 6846 . . . . . . . . . . . . . 14 (𝑝 = ∅ → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
3126, 27, 30ifbieq12d 4514 . . . . . . . . . . . . 13 (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
32 eqid 2736 . . . . . . . . . . . . 13 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))
33 fvex 6855 . . . . . . . . . . . . . 14 (𝑓‘∅) ∈ V
34 fvex 6855 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈ V
3533, 34ifex 4536 . . . . . . . . . . . . 13 if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V
3631, 32, 35fvmpt 6948 . . . . . . . . . . . 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 481 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ ω)
3938, 9syl 17 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑛)
40 0elsuc 7770 . . . . . . . . . . . . 13 (Ord 𝑛 → ∅ ∈ suc 𝑛)
4139, 40syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
4241iftrued 4494 . . . . . . . . . . 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 7390 . . . . . . . . . . . . 13 (𝑛 +o 𝑚) ∈ V
4746sucid 6399 . . . . . . . . . . . 12 (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚)
48 eleq1 2825 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛))
49 fveq2 6842 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑓𝑝) = (𝑓‘(𝑛 +o 𝑚)))
50 eqeq2 2748 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
5150riotabidv 7315 . . . . . . . . . . . . . . 15 (𝑝 = (𝑛 +o 𝑚) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
5251fveq2d 6846 . . . . . . . . . . . . . 14 (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
5348, 49, 52ifbieq12d 4514 . . . . . . . . . . . . 13 (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
54 fvex 6855 . . . . . . . . . . . . . 14 (𝑓‘(𝑛 +o 𝑚)) ∈ V
55 fvex 6855 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V
5654, 55ifex 4536 . . . . . . . . . . . . 13 if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V
5753, 32, 56fvmpt 6948 . . . . . . . . . . . 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 8412 . . . . . . . . . . . . . . . . . 18 1o = suc ∅
6059difeq2i 4079 . . . . . . . . . . . . . . . . 17 (ω ∖ 1o) = (ω ∖ suc ∅)
6160eleq2i 2829 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62 peano1 7825 . . . . . . . . . . . . . . . . 17 ∅ ∈ ω
63 eldifsucnn 8610 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
6462, 63ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65 dif0 4332 . . . . . . . . . . . . . . . . 17 (ω ∖ ∅) = ω
6665rexeqi 3312 . . . . . . . . . . . . . . . 16 (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
6761, 64, 663bitri 296 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
6860eleq2i 2829 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69 eldifsucnn 8610 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
7062, 69ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
7165rexeqi 3312 . . . . . . . . . . . . . . . 16 (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
7268, 70, 713bitri 296 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
7367, 72anbi12i 627 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74 reeanv 3217 . . . . . . . . . . . . . 14 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
7573, 74bitr4i 277 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦))
76 peano2 7827 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77 nnaword1 8576 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
7876, 77sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
7976adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80 nnord 7810 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑥 ∈ ω → Ord suc 𝑥)
8179, 80syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82 nnacl 8558 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
8376, 82sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84 nnord 7810 . . . . . . . . . . . . . . . . . . . 20 ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
8583, 84syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86 ordsucsssuc 7758 . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))
89 nnasuc 8553 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
9076, 89sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
9188, 90sseqtrrd 3985 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92 peano2 7827 . . . . . . . . . . . . . . . . . . 19 (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
9379, 92syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94 nnord 7810 . . . . . . . . . . . . . . . . . 18 (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96 peano2 7827 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97 nnacl 8558 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
9876, 96, 97syl2an 596 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99 nnord 7810 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o suc 𝑦))
101 ordtri1 6350 . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)
104 oveq12 7366 . . . . . . . . . . . . . . . . 17 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105 suceq 6383 . . . . . . . . . . . . . . . . . 18 (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106105adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107104, 106eleq12d 2832 . . . . . . . . . . . . . . . 16 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → ((𝑛 +o 𝑚) ∈ suc 𝑛 ↔ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
108107notbid 317 . . . . . . . . . . . . . . 15 ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → (¬ (𝑛 +o 𝑚) ∈ suc 𝑛 ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
109103, 108syl5ibrcom 246 . . . . . . . . . . . . . 14 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛))
110109rexlimivv 3196 . . . . . . . . . . . . 13 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
11175, 110sylbi 216 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112111iffalsed 4497 . . . . . . . . . . 11 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
1133adantl 482 . . . . . . . . . . . . 13 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑚 ∈ ω)
11438adantr 481 . . . . . . . . . . . . . 14 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑛 ∈ ω)
115 simpr 485 . . . . . . . . . . . . . 14 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑞 ∈ ω)
116113adantr 481 . . . . . . . . . . . . . 14 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑚 ∈ ω)
117 nnacan 8575 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118114, 115, 116, 117syl3anc 1371 . . . . . . . . . . . . 13 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119113, 118riota5 7343 . . . . . . . . . . . 12 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120119fveq2d 6846 . . . . . . . . . . 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 6842 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → (𝑓𝑎) = (𝑓𝑐))
126 suceq 6383 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
127126fveq2d 6846 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128125, 127breq12d 5118 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑐 → ((𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓𝑐)𝑅(𝑓‘suc 𝑐)))
129128rspcv 3577 . . . . . . . . . . . . . . 15 (𝑐𝑛 → (∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓𝑐)𝑅(𝑓‘suc 𝑐)))
130124, 129mpan9 507 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → (𝑓𝑐)𝑅(𝑓‘suc 𝑐))
131 elelsuc 6390 . . . . . . . . . . . . . . . 16 (𝑐𝑛𝑐 ∈ suc 𝑛)
132131adantl 482 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → 𝑐 ∈ suc 𝑛)
133132iftrued 4494 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓𝑐))
134 ordsucelsuc 7757 . . . . . . . . . . . . . . . . . 18 (Ord 𝑛 → (𝑐𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
13539, 134syl 17 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
136135adantr 481 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
137136biimpa 477 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → suc 𝑐 ∈ suc 𝑛)
138137iftrued 4494 . . . . . . . . . . . . . 14 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139130, 133, 1383brtr4d 5137 . . . . . . . . . . . . 13 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
140139adantlr 713 . . . . . . . . . . . 12 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
14139adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord 𝑛)
1425adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 +o 𝑚) ∈ ω)
143 elnn 7813 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144143ancoms 459 . . . . . . . . . . . . . . . . . . 19 (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145142, 144sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146 nnord 7810 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ω → Ord 𝑐)
147145, 146syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148 ordtri3or 6349 . . . . . . . . . . . . . . . . 17 ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛𝑐𝑛 = 𝑐𝑐𝑛))
149141, 147, 148syl2an2r 683 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛𝑐𝑛 = 𝑐𝑐𝑛))
150 3orel3 1486 . . . . . . . . . . . . . . . 16 𝑐𝑛 → ((𝑛𝑐𝑛 = 𝑐𝑐𝑛) → (𝑛𝑐𝑛 = 𝑐)))
151149, 150syl5com 31 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐𝑛 → (𝑛𝑐𝑛 = 𝑐)))
152 fveq2 6842 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔𝑏) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
153 suceq 6383 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
154153fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155152, 154breq12d 5118 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156 simprr3 1223 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))
157156adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))
158157adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))
159 ordelss 6333 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord 𝑐𝑛𝑐) → 𝑛𝑐)
160147, 159sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑛𝑐)
16138adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → 𝑛 ∈ ω)
162161adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑛 ∈ ω)
163145adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑐 ∈ ω)
164 nnawordex 8584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
165162, 163, 164syl2an2r 683 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
166160, 165mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
167 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168167eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169168cbvrexvw 3226 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170166, 169sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
171 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐)
172 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω)
1753ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑚 ∈ ω)
176175adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑚 ∈ ω)
177162adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑛 ∈ ω)
178177adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑛 ∈ ω)
179 nnaord 8566 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180174, 176, 178, 179syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑝𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
181173, 180mpbird 256 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝𝑚)
182170, 181, 171reximssdv 3169 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝𝑚 (𝑛 +o 𝑝) = 𝑐)
183 elnn 7813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑚𝑚 ∈ ω) → 𝑝 ∈ ω)
184183ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ ω ∧ 𝑝𝑚) → 𝑝 ∈ ω)
185175, 184sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → 𝑝 ∈ ω)
186 nnasmo 8609 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187177, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188 reu5 3355 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
189166, 187, 188sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
190189adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
191168riota2 7339 . . . . . . . . . . . . . . . . . . . . . . . 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 286 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝𝑚) → ((𝑛 +o 𝑝) = 𝑐𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195194rexbidva 3173 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (∃𝑝𝑚 (𝑛 +o 𝑝) = 𝑐 ↔ ∃𝑝𝑚 𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
196182, 195mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃𝑝𝑚 𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
197 risset 3221 . . . . . . . . . . . . . . . . . . . 20 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝𝑚 𝑝 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
198196, 197sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚)
199155, 158, 198rspcdva 3582 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
200 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → 𝑛𝑐)
201 vex 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ V
202147adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → Ord 𝑐)
203 ordelsuc 7755 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛𝑐 ↔ suc 𝑛𝑐))
204201, 202, 203sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ suc 𝑛𝑐))
205 peano2 7827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
20638, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207 nnord 7810 . . . . . . . . . . . . . . . . . . . . . . . . 25 (suc 𝑛 ∈ ω → Ord suc 𝑛)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord suc 𝑛)
209208adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord suc 𝑛)
210209adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord suc 𝑛)
211 ordtri1 6350 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord suc 𝑛 ∧ Ord 𝑐) → (suc 𝑛𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
212210, 202, 211syl2an2r 683 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (suc 𝑛𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
213204, 212bitrd 278 . . . . . . . . . . . . . . . . . . . 20 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
214200, 213mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ¬ 𝑐 ∈ suc 𝑛)
215214iffalsed 4497 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216 riotacl 7331 . . . . . . . . . . . . . . . . . . . . . . 23 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217189, 216syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218 nnasuc 8553 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
219162, 217, 218syl2an2r 683 . . . . . . . . . . . . . . . . . . . . 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 7320 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
222 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞𝑛
223 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞 +o
224222, 223, 221nfov 7387 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑞(𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225224nfeq1 2922 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞(𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227226eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞 = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228221, 225, 227riota2f 7338 . . . . . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑛 +o (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐)
231 suceq 6383 . . . . . . . . . . . . . . . . . . . . . 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 7827 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235217, 234syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
236 peano2 7827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ω → suc 𝑝 ∈ ω)
237 nnasuc 8553 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
238177, 237sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240239eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)))
241240rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((suc 𝑝 ∈ ω ∧ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
242236, 238, 241syl2an2 684 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
243 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244243eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245244rexbidv 3175 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
246242, 245syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . 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 8609 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250177, 249syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251 reu5 3355 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252248, 250, 251sylanbrc 583 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253221nfsuc 6389 . . . . . . . . . . . . . . . . . . . . . 22 𝑞 suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254222, 223, 253nfov 7387 . . . . . . . . . . . . . . . . . . . . . . 23 𝑞(𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255254nfeq1 2922 . . . . . . . . . . . . . . . . . . . . . 22 𝑞(𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257256eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258253, 255, 257riota2f 7338 . . . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . . . 19 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
261260fveq2d 6846 . . . . . . . . . . . . . . . . . 18 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262199, 215, 2613brtr4d 5137 . . . . . . . . . . . . . . . . 17 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
263262ex 413 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
264 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → (𝑔𝑏) = (𝑔‘∅))
265 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = ∅ → suc 𝑏 = suc ∅)
266265, 59eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = ∅ → suc 𝑏 = 1o)
267266fveq2d 6846 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268264, 267breq12d 5118 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ∅ → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269 eldif 3920 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270 nnord 7810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ω → Ord 𝑚)
271 ordtri1 6350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 1o ∧ Ord 𝑚) → (1o𝑚 ↔ ¬ 𝑚 ∈ 1o))
2728, 270, 271sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ ω → (1o𝑚 ↔ ¬ 𝑚 ∈ 1o))
273272biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o) → 1o𝑚)
274269, 273sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (ω ∖ 1o) → 1o𝑚)
275274adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o𝑚)
27659, 275eqsstrrid 3993 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277 0ex 5264 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
278113, 270syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279 ordelsuc 7755 . . . . . . . . . . . . . . . . . . . . . . 23 ((∅ ∈ V ∧ Ord 𝑚) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
280277, 278, 279sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
281276, 280mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ 𝑚)
282281adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∅ ∈ 𝑚)
283268, 156, 282rspcdva 3582 . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓𝑛) = (𝑔‘∅))
288 nnon 7808 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → 𝑛 ∈ On)
28938, 288syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290 oa1suc 8477 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291289, 290syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292 1onn 8586 . . . . . . . . . . . . . . . . . . . . . . 23 1o ∈ ω
293 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294293eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛))
295294rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
296292, 291, 295sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
297 nnasmo 8609 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
29838, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299 reu5 3355 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300296, 298, 299sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301294riota2 7339 . . . . . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
304303adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
305304fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306283, 287, 3053brtr4d 5137 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓𝑛)𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307201sucid 6399 . . . . . . . . . . . . . . . . . . . . 21 𝑛 ∈ suc 𝑛
308307iftruei 4493 . . . . . . . . . . . . . . . . . . . 20 if(𝑛 ∈ suc 𝑛, (𝑓𝑛), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓𝑛)
309 eleq1 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛𝑐 ∈ suc 𝑛))
310 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → (𝑓𝑛) = (𝑓𝑐))
311309, 310ifbieq1d 4510 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓𝑛), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312308, 311eqtr3id 2790 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑐 → (𝑓𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313 suceq 6383 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314313eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315314riotabidv 7315 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316315fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317312, 316breq12d 5118 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑐 → ((𝑓𝑛)𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) ↔ if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
318306, 317syl5ibcom 244 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
319318adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
320263, 319jaod 857 . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . 13 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
323135notbid 317 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (¬ 𝑐𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
324323adantr 481 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (¬ 𝑐𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
325324adantr 481 . . . . . . . . . . . . . . 15 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
326325biimpa 477 . . . . . . . . . . . . . 14 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → ¬ suc 𝑐 ∈ suc 𝑛)
327326iffalsed 4497 . . . . . . . . . . . . 13 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328322, 327breqtrrd 5133 . . . . . . . . . . . 12 (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329140, 328pm2.61dan 811 . . . . . . . . . . 11 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
330 elelsuc 6390 . . . . . . . . . . . . 13 (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚))
331330adantl 482 . . . . . . . . . . . 12 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚))
332 eleq1 2825 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛𝑐 ∈ suc 𝑛))
333 fveq2 6842 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑓𝑝) = (𝑓𝑐))
334 eqeq2 2748 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐))
335334riotabidv 7315 . . . . . . . . . . . . . . 15 (𝑝 = 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336335fveq2d 6846 . . . . . . . . . . . . . 14 (𝑝 = 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337332, 333, 336ifbieq12d 4514 . . . . . . . . . . . . 13 (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338 fvex 6855 . . . . . . . . . . . . . 14 (𝑓𝑐) ∈ V
339 fvex 6855 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340338, 339ifex 4536 . . . . . . . . . . . . 13 if(𝑐 ∈ suc 𝑛, (𝑓𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V
341337, 32, 340fvmpt 6948 . . . . . . . . . . . 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 7757 . . . . . . . . . . . . . . 15 (Ord (𝑛 +o 𝑚) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
34419, 343syl 17 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
345344adantr 481 . . . . . . . . . . . . 13 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
346345biimpa 477 . . . . . . . . . . . 12 ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → suc 𝑐 ∈ suc (𝑛 +o 𝑚))
347 eleq1 2825 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348 fveq2 6842 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑓𝑝) = (𝑓‘suc 𝑐))
349 eqeq2 2748 . . . . . . . . . . . . . . . 16 (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350349riotabidv 7315 . . . . . . . . . . . . . . 15 (𝑝 = suc 𝑐 → (𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351350fveq2d 6846 . . . . . . . . . . . . . 14 (𝑝 = suc 𝑐 → (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352347, 348, 351ifbieq12d 4514 . . . . . . . . . . . . 13 (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
353 fvex 6855 . . . . . . . . . . . . . 14 (𝑓‘suc 𝑐) ∈ V
354 fvex 6855 . . . . . . . . . . . . . 14 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V
355353, 354ifex 4536 . . . . . . . . . . . . 13 if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V
356352, 32, 355fvmpt 6948 . . . . . . . . . . . 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 5137 . . . . . . . . . 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 6855 . . . . . . . . . . . 12 (𝑓𝑝) ∈ V
361 fvex 6855 . . . . . . . . . . . 12 (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V
362360, 361ifex 4536 . . . . . . . . . . 11 if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363362, 32fnmpti 6644 . . . . . . . . . 10 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
36446sucex 7741 . . . . . . . . . . . 12 suc (𝑛 +o 𝑚) ∈ V
365364mptex 7173 . . . . . . . . . . 11 (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V
366 fneq1 6593 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ( Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)))
367 fveq1 6841 . . . . . . . . . . . . . 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 6841 . . . . . . . . . . . . . 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 631 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)))
372 fveq1 6841 . . . . . . . . . . . . . 14 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐))
373 fveq1 6841 . . . . . . . . . . . . . 14 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (‘suc 𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
374372, 373breq12d 5118 . . . . . . . . . . . . 13 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((𝑐)𝑅(‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
375374ralbidv 3174 . . . . . . . . . . . 12 ( = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓𝑝), (𝑔‘(𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
376366, 371, 3753anbi123d 1436 . . . . . . . . . . 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 3565 . . . . . . . . . 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 1448 . . . . . . . . 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 836 . . . . . . . 8 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐)))
380 suceq 6383 . . . . . . . . . . . 12 (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381380fneq2d 6596 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → ( Fn suc 𝑝 Fn suc (𝑛 +o 𝑚)))
382 fveqeq2 6851 . . . . . . . . . . . 12 (𝑝 = (𝑛 +o 𝑚) → ((𝑝) = 𝑦 ↔ (‘(𝑛 +o 𝑚)) = 𝑦))
383382anbi2d 629 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → (((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ↔ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦)))
384 raleq 3309 . . . . . . . . . . 11 (𝑝 = (𝑛 +o 𝑚) → (∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐)))
385381, 383, 3843anbi123d 1436 . . . . . . . . . 10 (𝑝 = (𝑛 +o 𝑚) → (( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)) ↔ ( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))))
386385exbidv 1924 . . . . . . . . 9 (𝑝 = (𝑛 +o 𝑚) → (∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)) ↔ ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))))
387386rspcev 3581 . . . . . . . 8 (((𝑛 +o 𝑚) ∈ (ω ∖ 1o) ∧ ∃( Fn suc (𝑛 +o 𝑚) ∧ ((‘∅) = 𝑥 ∧ (‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(𝑐)𝑅(‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
38823, 379, 387syl2an2r 683 . . . . . . 7 (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
389388ex 413 . . . . . 6 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐))))
390389exlimdvv 1937 . . . . 5 ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐))))
391390rexlimivv 3196 . . . 4 (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
392391exlimiv 1933 . . 3 (∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
393 vex 3449 . . . . 5 𝑥 ∈ V
394 vex 3449 . . . . 5 𝑦 ∈ V
395393, 394opelco 5827 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧𝑧t++𝑅𝑦))
396 reeanv 3217 . . . . . 6 (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
397 eeanv 2345 . . . . . . 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 9649 . . . . . . 7 (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
400 brttrcl 9649 . . . . . . 7 (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
401399, 400anbi12i 627 . . . . . 6 ((𝑥t++𝑅𝑧𝑧t++𝑅𝑦) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
402396, 398, 4013bitr4ri 303 . . . . 5 ((𝑥t++𝑅𝑧𝑧t++𝑅𝑦) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
403402exbii 1850 . . . 4 (∃𝑧(𝑥t++𝑅𝑧𝑧t++𝑅𝑦) ↔ ∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
404395, 403bitri 274 . . 3 (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑧) ∧ ∀𝑎𝑛 (𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔𝑚) = 𝑦) ∧ ∀𝑏𝑚 (𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
405 df-br 5106 . . . 4 (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406 brttrcl 9649 . . . 4 (𝑥t++𝑅𝑦 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
407405, 406bitr3i 276 . . 3 (⟨𝑥, 𝑦⟩ ∈ t++𝑅 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃( Fn suc 𝑝 ∧ ((‘∅) = 𝑥 ∧ (𝑝) = 𝑦) ∧ ∀𝑐𝑝 (𝑐)𝑅(‘suc 𝑐)))
408392, 404, 4073imtr4i 291 . 2 (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
4091, 408relssi 5743 1 (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  ∃!wreu 3351  ∃*wrmo 3352  Vcvv 3445  cdif 3907  wss 3910  c0 4282  ifcif 4486  cop 4592   class class class wbr 5105  cmpt 5188  ccom 5637  Ord word 6316  Oncon0 6317  suc csuc 6319   Fn wfn 6491  cfv 6496  crio 7312  (class class class)co 7357  ωcom 7802  1oc1o 8405   +o coa 8409  t++cttrcl 9643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-ttrcl 9644
This theorem is referenced by:  ttrclco  9654  cottrcl  9655  dfttrcl2  9660  frmin  9685  frrlem16  9694
  Copyright terms: Public domain W3C validator