Theorem ttrcltr 9698

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.

Step	Hyp	Ref	Expression
1		relco 6108	. 2 ⊢ Rel (t++𝑅 ∘ t++𝑅)
2		eldifi 4081	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3		eldifi 4081	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4		nnacl 8602	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
5	2, 3, 4	syl2an 608	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6		eldif 3912	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7		1on 8471	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
8	7	onordi 6475	. . . . . . . . . . . . . . 15 ⊢ Ord 1o
9		nnord 7873	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → Ord 𝑛)
10		ordtri1 6395	. . . . . . . . . . . . . . 15 ⊢ ((Ord 1o ∧ Ord 𝑛) → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
11	8, 9, 10	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
12	11	biimpar 483	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o) → 1o ⊆ 𝑛)
13	6, 12	sylbi 220	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → 1o ⊆ 𝑛)
14	13	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑛)
15		nnaword1 8620	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
16	2, 3, 15	syl2an 608	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
17	14, 16	sstrd 3944	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18		nnord 7873	. . . . . . . . . . . 12 ⊢ ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
19	5, 18	syl 18	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20		ordtri1 6395	. . . . . . . . . . 11 ⊢ ((Ord 1o ∧ Ord (𝑛 +o 𝑚)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
21	8, 19, 20	sylancr 599	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
22	17, 21	mpbid 235	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o)
23	5, 22	eldifd 3913	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24		0elsuc 7834	. . . . . . . . . . . . 13 ⊢ (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
25	19, 24	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26		eleq1 2850	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑓‘𝑝) = (𝑓‘∅))
28		eqeq2 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
29	28	riotabidv 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ∅ → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
30	29	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
31	26, 27, 30	ifbieq12d 4514	. . . . . . . . . . . . 13 ⊢ (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
32		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))
33		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑓‘∅) ∈ V
34		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈ V
35	33, 34	ifex 4536	. . . . . . . . . . . . 13 ⊢ if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V
36	31, 32, 35	fvmpt 6990	. . . . . . . . . . . 12 ⊢ (∅ ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
37	25, 36	syl 18	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
38	2	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ ω)
39	38, 9	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑛)
40		0elsuc 7834	. . . . . . . . . . . . 13 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
41	39, 40	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
42	41	iftrued 4493	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅))
43	37, 42	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅))
44		simpl2l 1245	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘∅) = 𝑥)
45	43, 44	sylan9eq 2817	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥)
46		ovex 7449	. . . . . . . . . . . . 13 ⊢ (𝑛 +o 𝑚) ∈ V
47	46	sucid 6446	. . . . . . . . . . . 12 ⊢ (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚)
48		eleq1 2850	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛))
49		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑓‘𝑝) = (𝑓‘(𝑛 +o 𝑚)))
50		eqeq2 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
51	50	riotabidv 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑛 +o 𝑚) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
52	51	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
53	48, 49, 52	ifbieq12d 4514	. . . . . . . . . . . . 13 ⊢ (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
54		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑓‘(𝑛 +o 𝑚)) ∈ V
55		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V
56	54, 55	ifex 4536	. . . . . . . . . . . . 13 ⊢ if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V
57	53, 32, 56	fvmpt 6990	. . . . . . . . . . . 12 ⊢ ((𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
58	47, 57	mp1i 14	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
59		df-1o 8458	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
60	59	difeq2i 4074	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
61	60	eleq2i 2854	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62		peano1 7888	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ ω
63		eldifsucnn 8655	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65		dif0 4330	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ ∅) = ω
66	65	rexeqi 3320	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
67	61, 64, 66	3bitri 300	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
68	60	eleq2i 2854	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69		eldifsucnn 8655	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
70	62, 69	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
71	65	rexeqi 3320	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
72	68, 70, 71	3bitri 300	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
73	67, 72	anbi12i 640	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74		reeanv 3236	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
75	73, 74	bitr4i 281	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦))
76		peano2 7889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77		nnaword1 8620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
78	76, 77	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
79	76	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80		nnord 7873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑥 ∈ ω → Ord suc 𝑥)
81	79, 80	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82		nnacl 8602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
83	76, 82	sylan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84		nnord 7873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
85	83, 84	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86		ordsucsssuc 7822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord suc 𝑥 ∧ Ord (suc 𝑥 +o 𝑦)) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
87	81, 85, 86	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
88	78, 87	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))
89		nnasuc 8597	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
90	76, 89	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
91	88, 90	sseqtrrd 3971	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92		peano2 7889	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
93	79, 92	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94		nnord 7873	. . . . . . . . . . . . . . . . . 18 ⊢ (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
95	93, 94	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96		peano2 7889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97		nnacl 8602	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
98	76, 96, 97	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99		nnord 7873	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
100	98, 99	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o suc 𝑦))
101		ordtri1 6395	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord suc suc 𝑥 ∧ Ord (suc 𝑥 +o suc 𝑦)) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
102	95, 100, 101	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
103	91, 102	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)
104		oveq12 7425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105		suceq 6430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106	105	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107	104, 106	eleq12d 2856	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ((𝑛 +o 𝑚) ∈ suc 𝑛 ↔ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
108	107	notbid 321	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (¬ (𝑛 +o 𝑚) ∈ suc 𝑛 ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
109	103, 108	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛))
110	109	rexlimivv 3206	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
111	75, 110	sylbi 220	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112	111	iffalsed 4496	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
113	3	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑚 ∈ ω)
114	38	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑛 ∈ ω)
115		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑞 ∈ ω)
116	113	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑚 ∈ ω)
117		nnacan 8619	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118	114, 115, 116, 117	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119	113, 118	riota5 7402	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120	119	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔‘𝑚))
121	58, 112, 120	3eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔‘𝑚))
122		simpr2r 1252	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘𝑚) = 𝑦)
123	121, 122	sylan9eq 2817	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)
124		simprl3 1239	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
125		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐))
126		suceq 6430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
127	126	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128	125, 127	breq12d 5120	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
129	128	rspcv 3575	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑛 → (∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
130	124, 129	mpan9 516	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐))
131		elelsuc 6437	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝑛 → 𝑐 ∈ suc 𝑛)
132	131	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → 𝑐 ∈ suc 𝑛)
133	132	iftrued 4493	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑐))
134		ordsucelsuc 7821	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑛 → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
135	39, 134	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
136	135	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
137	136	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → suc 𝑐 ∈ suc 𝑛)
138	137	iftrued 4493	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139	130, 133, 138	3brtr4d 5141	. . . . . . . . . . . . 13 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
140	139	adantlr 728	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
141	39	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord 𝑛)
142	5	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 +o 𝑚) ∈ ω)
143		elnn 7876	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144	143	ancoms 464	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145	142, 144	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146		nnord 7873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ω → Ord 𝑐)
147	145, 146	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148		ordtri3or 6394	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
149	141, 147, 148	syl2an2r 698	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
150		3orel3 1517	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑐 ∈ 𝑛 → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
151	149, 150	syl5com 32	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
152		fveq2 6882	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘𝑏) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
153		suceq 6430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
154	153	fveq2d 6886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155	152, 154	breq12d 5120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156		simprr3 1242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
157	156	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
158	157	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
159		ordelss 6377	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Ord 𝑐 ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
160	147, 159	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
161	38	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → 𝑛 ∈ ω)
162	161	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑛 ∈ ω)
163	145	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑐 ∈ ω)
164		nnawordex 8628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
165	162, 163, 164	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
166	160, 165	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
167		oveq2 7424	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168	167	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169	168	cbvrexvw 3243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170	166, 169	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
171		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐)
172		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑐 ∈ (𝑛 +o 𝑚))
173	171, 172	eqeltrd 2862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))
174		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω)
175	3	ad4antlr 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑚 ∈ ω)
176	175	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑚 ∈ ω)
177	162	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ ω)
178	177	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑛 ∈ ω)
179		nnaord 8610	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180	174, 176, 178, 179	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
181	173, 180	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ 𝑚)
182	170, 181, 171	reximssdv 3182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐)
183		elnn 7876	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑚 ∧ 𝑚 ∈ ω) → 𝑝 ∈ ω)
184	183	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
185	175, 184	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
186		nnasmo 8654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187	177, 186	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188		reu5 3369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
189	166, 187, 188	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
190	189	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
191	168	riota2 7398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
192	185, 190, 191	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
193		eqcom 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
194	192, 193	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195	194	rexbidva 3186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
196	182, 195	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
197		risset 3239	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
198	196, 197	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚)
199	155, 158, 198	rspcdva 3580	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
200		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ 𝑐)
201		vex 3457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑛 ∈ V
202	147	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → Ord 𝑐)
203		ordelsuc 7819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
204	201, 202, 203	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
205		peano2 7889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
206	38, 205	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207		nnord 7873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (suc 𝑛 ∈ ω → Ord suc 𝑛)
208	206, 207	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord suc 𝑛)
209	208	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord suc 𝑛)
210	209	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord suc 𝑛)
211		ordtri1 6395	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord suc 𝑛 ∧ Ord 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
212	210, 202, 211	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
213	204, 212	bitrd 282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
214	200, 213	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ¬ 𝑐 ∈ suc 𝑛)
215	214	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216		riotacl 7390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217	189, 216	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218		nnasuc 8597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
219	162, 217, 218	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
220		eqidd 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
221		nfriota1 7380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
222		nfcv 2924	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞𝑛
223		nfcv 2924	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞 +o
224	222, 223, 221	nfov 7446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225	224	nfeq1 2939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226		oveq2 7424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227	226	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228	221, 225, 227	riota2f 7397	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
229	217, 189, 228	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
230	220, 229	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐)
231		suceq 6430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 → suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
232	230, 231	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
233	219, 232	eqtrd 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
234		peano2 7889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235	217, 234	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
236		peano2 7889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ω → suc 𝑝 ∈ ω)
237		nnasuc 8597	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
238	177, 237	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239		oveq2 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240	239	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)))
241	240	rspcev 3579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((suc 𝑝 ∈ ω ∧ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
242	236, 238, 241	syl2an2 699	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
243		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244	243	eqeq2d 2773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245	244	rexbidv 3188	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
246	242, 245	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ((𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
247	246	rexlimdva 3165	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
248	170, 247	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
249		nnasmo 8654	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250	177, 249	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251		reu5 3369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252	248, 250, 251	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253	221	nfsuc 6436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞 suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254	222, 223, 253	nfov 7446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255	254	nfeq1 2939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256		oveq2 7424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257	256	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258	253, 255, 257	riota2f 7397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
259	235, 252, 258	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
260	233, 259	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
261	260	fveq2d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262	199, 215, 261	3brtr4d 5141	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
263	262	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
264		fveq2 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘𝑏) = (𝑔‘∅))
265		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅)
266	265, 59	eqtr4di 2815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ∅ → suc 𝑏 = 1o)
267	266	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268	264, 267	breq12d 5120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ∅ → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269		eldif 3912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270		nnord 7873	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ω → Ord 𝑚)
271		ordtri1 6395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 1o ∧ Ord 𝑚) → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
272	8, 270, 271	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ ω → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
273	272	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o) → 1o ⊆ 𝑚)
274	269, 273	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (ω ∖ 1o) → 1o ⊆ 𝑚)
275	274	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑚)
276	59, 275	eqsstrrid 3973	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277		0ex 5268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ∈ V
278	113, 270	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279		ordelsuc 7819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ V ∧ Ord 𝑚) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
280	277, 278, 279	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
281	276, 280	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ 𝑚)
282	281	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∅ ∈ 𝑚)
283	268, 156, 282	rspcdva 3580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘∅)𝑅(𝑔‘1o))
284		simpl2r 1246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = 𝑧)
285		simpr2l 1251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘∅) = 𝑧)
286	284, 285	eqtr4d 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = (𝑔‘∅))
287	286	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛) = (𝑔‘∅))
288		nnon 7871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
289	38, 288	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290		oa1suc 8521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291	289, 290	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292		1onn 8631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o ∈ ω
293		oveq2 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294	293	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛))
295	294	rspcev 3579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
296	292, 291, 295	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
297		nnasmo 8654	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
298	38, 297	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299		reu5 3369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300	296, 298, 299	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301	294	riota2 7398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1o ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
302	292, 300, 301	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
303	291, 302	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
304	303	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
305	304	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306	283, 287, 305	3brtr4d 5141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307	201	sucid 6446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ suc 𝑛
308	307	iftruei 4492	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑛)
309		eleq1 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
310		fveq2 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = (𝑓‘𝑐))
311	309, 310	ifbieq1d 4510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312	308, 311	eqtr3id 2811	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313		suceq 6430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314	313	eqeq2d 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315	314	riotabidv 7375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316	315	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317	312, 316	breq12d 5120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑐 → ((𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) ↔ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
318	306, 317	syl5ibcom 248	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
319	318	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
320	263, 319	jaod 873	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
321	151, 320	syld 48	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
322	321	imp 412	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
323	135	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
324	323	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
325	324	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
326	325	biimpa 482	. . . . . . . . . . . . . 14 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → ¬ suc 𝑐 ∈ suc 𝑛)
327	326	iffalsed 4496	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328	322, 327	breqtrrd 5137	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329	140, 328	pm2.61dan 825	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
330		elelsuc 6437	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚))
331	330	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚))
332		eleq1 2850	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
333		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑓‘𝑝) = (𝑓‘𝑐))
334		eqeq2 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐))
335	334	riotabidv 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336	335	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337	332, 333, 336	ifbieq12d 4514	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑐) ∈ V
339		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340	338, 339	ifex 4536	. . . . . . . . . . . . 13 ⊢ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V
341	337, 32, 340	fvmpt 6990	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
342	331, 341	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
343		ordsucelsuc 7821	. . . . . . . . . . . . . . 15 ⊢ (Ord (𝑛 +o 𝑚) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
344	19, 343	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
345	344	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
346	345	biimpa 482	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → suc 𝑐 ∈ suc (𝑛 +o 𝑚))
347		eleq1 2850	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑓‘𝑝) = (𝑓‘suc 𝑐))
349		eqeq2 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350	349	riotabidv 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = suc 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351	350	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352	347, 348, 351	ifbieq12d 4514	. . . . . . . . . . . . 13 ⊢ (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
353		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑓‘suc 𝑐) ∈ V
354		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V
355	353, 354	ifex 4536	. . . . . . . . . . . . 13 ⊢ if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V
356	352, 32, 355	fvmpt 6990	. . . . . . . . . . . 12 ⊢ (suc 𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
357	346, 356	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
358	329, 342, 357	3brtr4d 5141	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
359	358	ralrimiva 3156	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
360		fvex 6895	. . . . . . . . . . . 12 ⊢ (𝑓‘𝑝) ∈ V
361		fvex 6895	. . . . . . . . . . . 12 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V
362	360, 361	ifex 4536	. . . . . . . . . . 11 ⊢ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363	362, 32	fnmpti 6679	. . . . . . . . . 10 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
364	46	sucex 7808	. . . . . . . . . . . 12 ⊢ suc (𝑛 +o 𝑚) ∈ V
365	364	mptex 7225	. . . . . . . . . . 11 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V
366		fneq1 6627	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)))
367		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘∅) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅))
368	367	eqeq1d 2764	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘∅) = 𝑥 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥))
369		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘(𝑛 +o 𝑚)) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)))
370	369	eqeq1d 2764	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘(𝑛 +o 𝑚)) = 𝑦 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦))
371	368, 370	anbi12d 644	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)))
372		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐))
373		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘suc 𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
374	372, 373	breq12d 5120	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
375	374	ralbidv 3187	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
376	366, 371, 375	3anbi123d 1464	. . . . . . . . . . 11 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚) ∧ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))))
377	365, 376	spcev 3563	. . . . . . . . . 10 ⊢ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚) ∧ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
378	363, 377	mp3an1 1477	. . . . . . . . 9 ⊢ (((((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
379	45, 123, 359, 378	syl21anc 851	. . . . . . . 8 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
380		suceq 6430	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381	380	fneq2d 6630	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (ℎ Fn suc 𝑝 ↔ ℎ Fn suc (𝑛 +o 𝑚)))
382		fveqeq2 6891	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ‘𝑝) = 𝑦 ↔ (ℎ‘(𝑛 +o 𝑚)) = 𝑦))
383	382	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ↔ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦)))
384		raleq 3318	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
385	381, 383, 384	3anbi123d 1464	. . . . . . . . . 10 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ (ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
386	385	exbidv 1954	. . . . . . . . 9 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
387	386	rspcev 3579	. . . . . . . 8 ⊢ (((𝑛 +o 𝑚) ∈ (ω ∖ 1o) ∧ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
388	23, 379, 387	syl2an2r 698	. . . . . . 7 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
389	388	ex 418	. . . . . 6 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
390	389	exlimdvv 1967	. . . . 5 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
391	390	rexlimivv 3206	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
392	391	exlimiv 1963	. . 3 ⊢ (∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
393		vex 3457	. . . . 5 ⊢ 𝑥 ∈ V
394		vex 3457	. . . . 5 ⊢ 𝑦 ∈ V
395	393, 394	opelco 5855	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦))
396		reeanv 3236	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
397		eeanv 2380	. . . . . . 7 ⊢ (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
398	397	2rexbii 3140	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
399		brttrcl 9695	. . . . . . 7 ⊢ (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
400		brttrcl 9695	. . . . . . 7 ⊢ (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
401	399, 400	anbi12i 640	. . . . . 6 ⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
402	396, 398, 401	3bitr4ri 307	. . . . 5 ⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
403	402	exbii 1881	. . . 4 ⊢ (∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ ∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
404	395, 403	bitri 278	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
405		df-br 5108	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406		brttrcl 9695	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
407	405, 406	bitr3i 280	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
408	392, 404, 407	3imtr4i 295	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
409	1, 408	relssi 5771	1 ⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088  ∃!wreu 3365  ∃*wrmo 3366  Vcvv 3453   ∖ cdif 3899   ⊆ wss 3902  ∅c0 4282  ifcif 4485  ⟨cop 4593   class class class wbr 5107   ↦ cmpt 5190   ∘ ccom 5663  Ord word 6360  Oncon0 6361  suc csuc 6363   Fn wfn 6532  ‘cfv 6537  ℩crio 7372  (class class class)co 7416  ωcom 7865  1_oc1o 8451   +_o coa 8455  t++cttrcl 9689

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-oadd 8462  df-ttrcl 9690

This theorem is used by:  ttrclco  9700  cottrcl  9701  dfttrcl2  9706  frmin  9734  frrlem16  9743