Theorem ttrcltr 9713

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 6106	. 2 ⊢ Rel (t++𝑅 ∘ t++𝑅)
2		eldifi 4125	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3		eldifi 4125	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4		nnacl 8613	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
5	2, 3, 4	syl2an 594	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6		eldif 3957	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7		1on 8480	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
8	7	onordi 6474	. . . . . . . . . . . . . . 15 ⊢ Ord 1o
9		nnord 7865	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → Ord 𝑛)
10		ordtri1 6396	. . . . . . . . . . . . . . 15 ⊢ ((Ord 1o ∧ Ord 𝑛) → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
11	8, 9, 10	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
12	11	biimpar 476	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o) → 1o ⊆ 𝑛)
13	6, 12	sylbi 216	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → 1o ⊆ 𝑛)
14	13	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑛)
15		nnaword1 8631	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
16	2, 3, 15	syl2an 594	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
17	14, 16	sstrd 3991	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18		nnord 7865	. . . . . . . . . . . 12 ⊢ ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
19	5, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20		ordtri1 6396	. . . . . . . . . . 11 ⊢ ((Ord 1o ∧ Ord (𝑛 +o 𝑚)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
21	8, 19, 20	sylancr 585	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
22	17, 21	mpbid 231	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o)
23	5, 22	eldifd 3958	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24		0elsuc 7825	. . . . . . . . . . . . 13 ⊢ (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
25	19, 24	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26		eleq1 2819	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑓‘𝑝) = (𝑓‘∅))
28		eqeq2 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
29	28	riotabidv 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ∅ → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
30	29	fveq2d 6894	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
31	26, 27, 30	ifbieq12d 4555	. . . . . . . . . . . . 13 ⊢ (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
32		eqid 2730	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))
33		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑓‘∅) ∈ V
34		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈ V
35	33, 34	ifex 4577	. . . . . . . . . . . . 13 ⊢ if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V
36	31, 32, 35	fvmpt 6997	. . . . . . . . . . . 12 ⊢ (∅ ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
37	25, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
38	2	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ ω)
39	38, 9	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑛)
40		0elsuc 7825	. . . . . . . . . . . . 13 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
41	39, 40	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
42	41	iftrued 4535	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅))
43	37, 42	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅))
44		simpl2l 1224	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘∅) = 𝑥)
45	43, 44	sylan9eq 2790	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥)
46		ovex 7444	. . . . . . . . . . . . 13 ⊢ (𝑛 +o 𝑚) ∈ V
47	46	sucid 6445	. . . . . . . . . . . 12 ⊢ (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚)
48		eleq1 2819	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛))
49		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑓‘𝑝) = (𝑓‘(𝑛 +o 𝑚)))
50		eqeq2 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
51	50	riotabidv 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑛 +o 𝑚) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
52	51	fveq2d 6894	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
53	48, 49, 52	ifbieq12d 4555	. . . . . . . . . . . . 13 ⊢ (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
54		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑓‘(𝑛 +o 𝑚)) ∈ V
55		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V
56	54, 55	ifex 4577	. . . . . . . . . . . . 13 ⊢ if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V
57	53, 32, 56	fvmpt 6997	. . . . . . . . . . . 12 ⊢ ((𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
58	47, 57	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
59		df-1o 8468	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
60	59	difeq2i 4118	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
61	60	eleq2i 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62		peano1 7881	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ ω
63		eldifsucnn 8665	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65		dif0 4371	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ ∅) = ω
66	65	rexeqi 3322	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
67	61, 64, 66	3bitri 296	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
68	60	eleq2i 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69		eldifsucnn 8665	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
70	62, 69	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
71	65	rexeqi 3322	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
72	68, 70, 71	3bitri 296	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
73	67, 72	anbi12i 625	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74		reeanv 3224	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
75	73, 74	bitr4i 277	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦))
76		peano2 7883	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77		nnaword1 8631	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
78	76, 77	sylan 578	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
79	76	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80		nnord 7865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑥 ∈ ω → Ord suc 𝑥)
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82		nnacl 8613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
83	76, 82	sylan 578	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84		nnord 7865	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
85	83, 84	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86		ordsucsssuc 7813	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord suc 𝑥 ∧ Ord (suc 𝑥 +o 𝑦)) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
87	81, 85, 86	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
88	78, 87	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))
89		nnasuc 8608	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
90	76, 89	sylan 578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
91	88, 90	sseqtrrd 4022	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92		peano2 7883	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
93	79, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94		nnord 7865	. . . . . . . . . . . . . . . . . 18 ⊢ (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96		peano2 7883	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97		nnacl 8613	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
98	76, 96, 97	syl2an 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99		nnord 7865	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o suc 𝑦))
101		ordtri1 6396	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord suc suc 𝑥 ∧ Ord (suc 𝑥 +o suc 𝑦)) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
102	95, 100, 101	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
103	91, 102	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)
104		oveq12 7420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105		suceq 6429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106	105	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107	104, 106	eleq12d 2825	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ((𝑛 +o 𝑚) ∈ suc 𝑛 ↔ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
108	107	notbid 317	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (¬ (𝑛 +o 𝑚) ∈ suc 𝑛 ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
109	103, 108	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛))
110	109	rexlimivv 3197	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
111	75, 110	sylbi 216	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112	111	iffalsed 4538	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
113	3	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑚 ∈ ω)
114	38	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑛 ∈ ω)
115		simpr 483	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑞 ∈ ω)
116	113	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑚 ∈ ω)
117		nnacan 8630	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118	114, 115, 116, 117	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119	113, 118	riota5 7397	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120	119	fveq2d 6894	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔‘𝑚))
121	58, 112, 120	3eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔‘𝑚))
122		simpr2r 1231	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘𝑚) = 𝑦)
123	121, 122	sylan9eq 2790	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)
124		simprl3 1218	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
125		fveq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐))
126		suceq 6429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
127	126	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128	125, 127	breq12d 5160	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
129	128	rspcv 3607	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑛 → (∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
130	124, 129	mpan9 505	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐))
131		elelsuc 6436	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝑛 → 𝑐 ∈ suc 𝑛)
132	131	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → 𝑐 ∈ suc 𝑛)
133	132	iftrued 4535	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑐))
134		ordsucelsuc 7812	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑛 → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
135	39, 134	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
136	135	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
137	136	biimpa 475	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → suc 𝑐 ∈ suc 𝑛)
138	137	iftrued 4535	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139	130, 133, 138	3brtr4d 5179	. . . . . . . . . . . . 13 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
140	139	adantlr 711	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
141	39	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord 𝑛)
142	5	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 +o 𝑚) ∈ ω)
143		elnn 7868	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144	143	ancoms 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145	142, 144	sylan 578	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146		nnord 7865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ω → Ord 𝑐)
147	145, 146	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148		ordtri3or 6395	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
149	141, 147, 148	syl2an2r 681	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
150		3orel3 1484	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑐 ∈ 𝑛 → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
151	149, 150	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
152		fveq2 6890	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘𝑏) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
153		suceq 6429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
154	153	fveq2d 6894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155	152, 154	breq12d 5160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156		simprr3 1221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
157	156	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
158	157	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
159		ordelss 6379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Ord 𝑐 ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
160	147, 159	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
161	38	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → 𝑛 ∈ ω)
162	161	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑛 ∈ ω)
163	145	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑐 ∈ ω)
164		nnawordex 8639	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
165	162, 163, 164	syl2an2r 681	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
166	160, 165	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
167		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168	167	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169	168	cbvrexvw 3233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170	166, 169	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
171		simprr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐)
172		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑐 ∈ (𝑛 +o 𝑚))
173	171, 172	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))
174		simprl 767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω)
175	3	ad4antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑚 ∈ ω)
176	175	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑚 ∈ ω)
177	162	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ ω)
178	177	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑛 ∈ ω)
179		nnaord 8621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180	174, 176, 178, 179	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
181	173, 180	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ 𝑚)
182	170, 181, 171	reximssdv 3170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐)
183		elnn 7868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑚 ∧ 𝑚 ∈ ω) → 𝑝 ∈ ω)
184	183	ancoms 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
185	175, 184	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
186		nnasmo 8664	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187	177, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188		reu5 3376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
189	166, 187, 188	sylanbrc 581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
190	189	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
191	168	riota2 7393	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
192	185, 190, 191	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
193		eqcom 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
194	192, 193	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195	194	rexbidva 3174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
196	182, 195	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
197		risset 3228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
198	196, 197	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚)
199	155, 158, 198	rspcdva 3612	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
200		simpr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ 𝑐)
201		vex 3476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑛 ∈ V
202	147	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → Ord 𝑐)
203		ordelsuc 7810	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
204	201, 202, 203	sylancr 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
205		peano2 7883	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
206	38, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207		nnord 7865	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (suc 𝑛 ∈ ω → Ord suc 𝑛)
208	206, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord suc 𝑛)
209	208	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord suc 𝑛)
210	209	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord suc 𝑛)
211		ordtri1 6396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord suc 𝑛 ∧ Ord 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
212	210, 202, 211	syl2an2r 681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
213	204, 212	bitrd 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
214	200, 213	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ¬ 𝑐 ∈ suc 𝑛)
215	214	iffalsed 4538	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216		riotacl 7385	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217	189, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218		nnasuc 8608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
219	162, 217, 218	syl2an2r 681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
220		eqidd 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
221		nfriota1 7374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
222		nfcv 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞𝑛
223		nfcv 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞 +o
224	222, 223, 221	nfov 7441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225	224	nfeq1 2916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227	226	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228	221, 225, 227	riota2f 7392	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
229	217, 189, 228	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
230	220, 229	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐)
231		suceq 6429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 → suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
233	219, 232	eqtrd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
234		peano2 7883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235	217, 234	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
236		peano2 7883	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ω → suc 𝑝 ∈ ω)
237		nnasuc 8608	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
238	177, 237	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240	239	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)))
241	240	rspcev 3611	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((suc 𝑝 ∈ ω ∧ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
242	236, 238, 241	syl2an2 682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
243		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244	243	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245	244	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
246	242, 245	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ((𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
247	246	rexlimdva 3153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
248	170, 247	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
249		nnasmo 8664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250	177, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251		reu5 3376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252	248, 250, 251	sylanbrc 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253	221	nfsuc 6435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞 suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254	222, 223, 253	nfov 7441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255	254	nfeq1 2916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257	256	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258	253, 255, 257	riota2f 7392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
259	235, 252, 258	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
260	233, 259	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
261	260	fveq2d 6894	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262	199, 215, 261	3brtr4d 5179	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
263	262	ex 411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
264		fveq2 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘𝑏) = (𝑔‘∅))
265		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅)
266	265, 59	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ∅ → suc 𝑏 = 1o)
267	266	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268	264, 267	breq12d 5160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ∅ → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269		eldif 3957	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270		nnord 7865	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ω → Ord 𝑚)
271		ordtri1 6396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 1o ∧ Ord 𝑚) → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
272	8, 270, 271	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ ω → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
273	272	biimpar 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o) → 1o ⊆ 𝑚)
274	269, 273	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (ω ∖ 1o) → 1o ⊆ 𝑚)
275	274	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑚)
276	59, 275	eqsstrrid 4030	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277		0ex 5306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ∈ V
278	113, 270	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279		ordelsuc 7810	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ V ∧ Ord 𝑚) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
280	277, 278, 279	sylancr 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
281	276, 280	mpbird 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ 𝑚)
282	281	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∅ ∈ 𝑚)
283	268, 156, 282	rspcdva 3612	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘∅)𝑅(𝑔‘1o))
284		simpl2r 1225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = 𝑧)
285		simpr2l 1230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘∅) = 𝑧)
286	284, 285	eqtr4d 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = (𝑔‘∅))
287	286	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛) = (𝑔‘∅))
288		nnon 7863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
289	38, 288	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290		oa1suc 8533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291	289, 290	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292		1onn 8641	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o ∈ ω
293		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294	293	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛))
295	294	rspcev 3611	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
296	292, 291, 295	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
297		nnasmo 8664	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
298	38, 297	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299		reu5 3376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300	296, 298, 299	sylanbrc 581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301	294	riota2 7393	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1o ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
302	292, 300, 301	sylancr 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
303	291, 302	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
304	303	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
305	304	fveq2d 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306	283, 287, 305	3brtr4d 5179	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307	201	sucid 6445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ suc 𝑛
308	307	iftruei 4534	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑛)
309		eleq1 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
310		fveq2 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = (𝑓‘𝑐))
311	309, 310	ifbieq1d 4551	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312	308, 311	eqtr3id 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313		suceq 6429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314	313	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315	314	riotabidv 7369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316	315	fveq2d 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317	312, 316	breq12d 5160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑐 → ((𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) ↔ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
318	306, 317	syl5ibcom 244	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
319	318	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
320	263, 319	jaod 855	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
321	151, 320	syld 47	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
322	321	imp 405	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
323	135	notbid 317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
324	323	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
325	324	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
326	325	biimpa 475	. . . . . . . . . . . . . 14 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → ¬ suc 𝑐 ∈ suc 𝑛)
327	326	iffalsed 4538	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328	322, 327	breqtrrd 5175	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329	140, 328	pm2.61dan 809	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
330		elelsuc 6436	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚))
331	330	adantl 480	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚))
332		eleq1 2819	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
333		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑓‘𝑝) = (𝑓‘𝑐))
334		eqeq2 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐))
335	334	riotabidv 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336	335	fveq2d 6894	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337	332, 333, 336	ifbieq12d 4555	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑐) ∈ V
339		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340	338, 339	ifex 4577	. . . . . . . . . . . . 13 ⊢ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V
341	337, 32, 340	fvmpt 6997	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
342	331, 341	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
343		ordsucelsuc 7812	. . . . . . . . . . . . . . 15 ⊢ (Ord (𝑛 +o 𝑚) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
344	19, 343	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
345	344	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
346	345	biimpa 475	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → suc 𝑐 ∈ suc (𝑛 +o 𝑚))
347		eleq1 2819	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑓‘𝑝) = (𝑓‘suc 𝑐))
349		eqeq2 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350	349	riotabidv 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = suc 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351	350	fveq2d 6894	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352	347, 348, 351	ifbieq12d 4555	. . . . . . . . . . . . 13 ⊢ (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
353		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑓‘suc 𝑐) ∈ V
354		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V
355	353, 354	ifex 4577	. . . . . . . . . . . . 13 ⊢ if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V
356	352, 32, 355	fvmpt 6997	. . . . . . . . . . . 12 ⊢ (suc 𝑐 ∈ suc (𝑛 +o 𝑚) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
357	346, 356	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
358	329, 342, 357	3brtr4d 5179	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
359	358	ralrimiva 3144	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
360		fvex 6903	. . . . . . . . . . . 12 ⊢ (𝑓‘𝑝) ∈ V
361		fvex 6903	. . . . . . . . . . . 12 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V
362	360, 361	ifex 4577	. . . . . . . . . . 11 ⊢ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363	362, 32	fnmpti 6692	. . . . . . . . . 10 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
364	46	sucex 7796	. . . . . . . . . . . 12 ⊢ suc (𝑛 +o 𝑚) ∈ V
365	364	mptex 7226	. . . . . . . . . . 11 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V
366		fneq1 6639	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)))
367		fveq1 6889	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘∅) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅))
368	367	eqeq1d 2732	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘∅) = 𝑥 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥))
369		fveq1 6889	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘(𝑛 +o 𝑚)) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)))
370	369	eqeq1d 2732	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘(𝑛 +o 𝑚)) = 𝑦 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦))
371	368, 370	anbi12d 629	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)))
372		fveq1 6889	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐))
373		fveq1 6889	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘suc 𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
374	372, 373	breq12d 5160	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
375	374	ralbidv 3175	. . . . . . . . . . . 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 1434	. . . . . . . . . . 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 3595	. . . . . . . . . 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 1446	. . . . . . . . 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 834	. . . . . . . 8 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
380		suceq 6429	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381	380	fneq2d 6642	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (ℎ Fn suc 𝑝 ↔ ℎ Fn suc (𝑛 +o 𝑚)))
382		fveqeq2 6899	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ‘𝑝) = 𝑦 ↔ (ℎ‘(𝑛 +o 𝑚)) = 𝑦))
383	382	anbi2d 627	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ↔ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦)))
384		raleq 3320	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
385	381, 383, 384	3anbi123d 1434	. . . . . . . . . 10 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ (ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
386	385	exbidv 1922	. . . . . . . . 9 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
387	386	rspcev 3611	. . . . . . . 8 ⊢ (((𝑛 +o 𝑚) ∈ (ω ∖ 1o) ∧ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
388	23, 379, 387	syl2an2r 681	. . . . . . 7 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
389	388	ex 411	. . . . . 6 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
390	389	exlimdvv 1935	. . . . 5 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
391	390	rexlimivv 3197	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
392	391	exlimiv 1931	. . 3 ⊢ (∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
393		vex 3476	. . . . 5 ⊢ 𝑥 ∈ V
394		vex 3476	. . . . 5 ⊢ 𝑦 ∈ V
395	393, 394	opelco 5870	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦))
396		reeanv 3224	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
397		eeanv 2343	. . . . . . 7 ⊢ (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
398	397	2rexbii 3127	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
399		brttrcl 9710	. . . . . . 7 ⊢ (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
400		brttrcl 9710	. . . . . . 7 ⊢ (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
401	399, 400	anbi12i 625	. . . . . 6 ⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
402	396, 398, 401	3bitr4ri 303	. . . . 5 ⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
403	402	exbii 1848	. . . 4 ⊢ (∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ ∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
404	395, 403	bitri 274	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
405		df-br 5148	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406		brttrcl 9710	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
407	405, 406	bitr3i 276	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
408	392, 404, 407	3imtr4i 291	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
409	1, 408	relssi 5786	1 ⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085   = wceq 1539  ∃wex 1779   ∈ wcel 2104  ∀wral 3059  ∃wrex 3068  ∃!wreu 3372  ∃*wrmo 3373  Vcvv 3472   ∖ cdif 3944   ⊆ wss 3947  ∅c0 4321  ifcif 4527  ⟨cop 4633   class class class wbr 5147   ↦ cmpt 5230   ∘ ccom 5679  Ord word 6362  Oncon0 6363  suc csuc 6365   Fn wfn 6537  ‘cfv 6542  ℩crio 7366  (class class class)co 7411  ωcom 7857  1_oc1o 8461   +_o coa 8465  t++cttrcl 9704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-ttrcl 9705

This theorem is referenced by:  ttrclco  9715  cottrcl  9716  dfttrcl2  9721  frmin  9746  frrlem16  9755