Theorem ttrcltr 9669

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 6079	. 2 ⊢ Rel (t++𝑅 ∘ t++𝑅)
2		eldifi 4094	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3		eldifi 4094	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4		nnacl 8575	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
5	2, 3, 4	syl2an 596	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6		eldif 3924	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7		1on 8446	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
8	7	onordi 6445	. . . . . . . . . . . . . . 15 ⊢ Ord 1o
9		nnord 7850	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → Ord 𝑛)
10		ordtri1 6365	. . . . . . . . . . . . . . 15 ⊢ ((Ord 1o ∧ Ord 𝑛) → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
11	8, 9, 10	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
12	11	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o) → 1o ⊆ 𝑛)
13	6, 12	sylbi 217	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → 1o ⊆ 𝑛)
14	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑛)
15		nnaword1 8593	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
16	2, 3, 15	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
17	14, 16	sstrd 3957	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18		nnord 7850	. . . . . . . . . . . 12 ⊢ ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
19	5, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20		ordtri1 6365	. . . . . . . . . . 11 ⊢ ((Ord 1o ∧ Ord (𝑛 +o 𝑚)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
21	8, 19, 20	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
22	17, 21	mpbid 232	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o)
23	5, 22	eldifd 3925	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24		0elsuc 7810	. . . . . . . . . . . . 13 ⊢ (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
25	19, 24	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑓‘𝑝) = (𝑓‘∅))
28		eqeq2 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
29	28	riotabidv 7346	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ∅ → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
30	29	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
31	26, 27, 30	ifbieq12d 4517	. . . . . . . . . . . . 13 ⊢ (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
32		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))
33		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑓‘∅) ∈ V
34		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈ V
35	33, 34	ifex 4539	. . . . . . . . . . . . 13 ⊢ if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V
36	31, 32, 35	fvmpt 6968	. . . . . . . . . . . 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 480	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ ω)
39	38, 9	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑛)
40		0elsuc 7810	. . . . . . . . . . . . 13 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
41	39, 40	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
42	41	iftrued 4496	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅))
43	37, 42	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅))
44		simpl2l 1227	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘∅) = 𝑥)
45	43, 44	sylan9eq 2784	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥)
46		ovex 7420	. . . . . . . . . . . . 13 ⊢ (𝑛 +o 𝑚) ∈ V
47	46	sucid 6416	. . . . . . . . . . . 12 ⊢ (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚)
48		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛))
49		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑓‘𝑝) = (𝑓‘(𝑛 +o 𝑚)))
50		eqeq2 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
51	50	riotabidv 7346	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑛 +o 𝑚) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
52	51	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
53	48, 49, 52	ifbieq12d 4517	. . . . . . . . . . . . 13 ⊢ (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
54		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑓‘(𝑛 +o 𝑚)) ∈ V
55		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V
56	54, 55	ifex 4539	. . . . . . . . . . . . 13 ⊢ if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V
57	53, 32, 56	fvmpt 6968	. . . . . . . . . . . 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 8434	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
60	59	difeq2i 4086	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
61	60	eleq2i 2820	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62		peano1 7865	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ ω
63		eldifsucnn 8628	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65		dif0 4341	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ ∅) = ω
66	65	rexeqi 3298	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
67	61, 64, 66	3bitri 297	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
68	60	eleq2i 2820	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69		eldifsucnn 8628	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
70	62, 69	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
71	65	rexeqi 3298	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
72	68, 70, 71	3bitri 297	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
73	67, 72	anbi12i 628	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74		reeanv 3209	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
75	73, 74	bitr4i 278	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦))
76		peano2 7866	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77		nnaword1 8593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
78	76, 77	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
79	76	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80		nnord 7850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑥 ∈ ω → Ord suc 𝑥)
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82		nnacl 8575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
83	76, 82	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84		nnord 7850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
85	83, 84	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86		ordsucsssuc 7798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord suc 𝑥 ∧ Ord (suc 𝑥 +o 𝑦)) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
87	81, 85, 86	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
88	78, 87	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))
89		nnasuc 8570	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
90	76, 89	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
91	88, 90	sseqtrrd 3984	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92		peano2 7866	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
93	79, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94		nnord 7850	. . . . . . . . . . . . . . . . . 18 ⊢ (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96		peano2 7866	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97		nnacl 8575	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
98	76, 96, 97	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99		nnord 7850	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o suc 𝑦))
101		ordtri1 6365	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord suc suc 𝑥 ∧ Ord (suc 𝑥 +o suc 𝑦)) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
102	95, 100, 101	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
103	91, 102	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)
104		oveq12 7396	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105		suceq 6400	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106	105	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107	104, 106	eleq12d 2822	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ((𝑛 +o 𝑚) ∈ suc 𝑛 ↔ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
108	107	notbid 318	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (¬ (𝑛 +o 𝑚) ∈ suc 𝑛 ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
109	103, 108	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛))
110	109	rexlimivv 3179	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
111	75, 110	sylbi 217	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112	111	iffalsed 4499	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
113	3	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑚 ∈ ω)
114	38	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑛 ∈ ω)
115		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑞 ∈ ω)
116	113	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → 𝑚 ∈ ω)
117		nnacan 8592	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118	114, 115, 116, 117	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119	113, 118	riota5 7373	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120	119	fveq2d 6862	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔‘𝑚))
121	58, 112, 120	3eqtrd 2768	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔‘𝑚))
122		simpr2r 1234	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘𝑚) = 𝑦)
123	121, 122	sylan9eq 2784	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)
124		simprl3 1221	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
125		fveq2 6858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐))
126		suceq 6400	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
127	126	fveq2d 6862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128	125, 127	breq12d 5120	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
129	128	rspcv 3584	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑛 → (∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
130	124, 129	mpan9 506	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐))
131		elelsuc 6407	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝑛 → 𝑐 ∈ suc 𝑛)
132	131	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → 𝑐 ∈ suc 𝑛)
133	132	iftrued 4496	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑐))
134		ordsucelsuc 7797	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑛 → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
135	39, 134	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
136	135	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
137	136	biimpa 476	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → suc 𝑐 ∈ suc 𝑛)
138	137	iftrued 4496	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139	130, 133, 138	3brtr4d 5139	. . . . . . . . . . . . 13 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
140	139	adantlr 715	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
141	39	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord 𝑛)
142	5	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 +o 𝑚) ∈ ω)
143		elnn 7853	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144	143	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145	142, 144	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146		nnord 7850	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ω → Ord 𝑐)
147	145, 146	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148		ordtri3or 6364	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
149	141, 147, 148	syl2an2r 685	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
150		3orel3 1488	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑐 ∈ 𝑛 → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
151	149, 150	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
152		fveq2 6858	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘𝑏) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
153		suceq 6400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
154	153	fveq2d 6862	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155	152, 154	breq12d 5120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156		simprr3 1224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
157	156	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
158	157	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))
159		ordelss 6348	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Ord 𝑐 ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
160	147, 159	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
161	38	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → 𝑛 ∈ ω)
162	161	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑛 ∈ ω)
163	145	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑐 ∈ ω)
164		nnawordex 8601	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
165	162, 163, 164	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
166	160, 165	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
167		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168	167	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169	168	cbvrexvw 3216	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170	166, 169	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
171		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐)
172		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑐 ∈ (𝑛 +o 𝑚))
173	171, 172	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))
174		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω)
175	3	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑚 ∈ ω)
176	175	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑚 ∈ ω)
177	162	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ ω)
178	177	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑛 ∈ ω)
179		nnaord 8583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180	174, 176, 178, 179	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
181	173, 180	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ 𝑚)
182	170, 181, 171	reximssdv 3151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐)
183		elnn 7853	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑚 ∧ 𝑚 ∈ ω) → 𝑝 ∈ ω)
184	183	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
185	175, 184	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
186		nnasmo 8627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187	177, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188		reu5 3356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
189	166, 187, 188	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
190	189	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
191	168	riota2 7369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
192	185, 190, 191	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
193		eqcom 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
194	192, 193	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195	194	rexbidva 3155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
196	182, 195	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
197		risset 3212	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
198	196, 197	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚)
199	155, 158, 198	rspcdva 3589	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
200		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → 𝑛 ∈ 𝑐)
201		vex 3451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑛 ∈ V
202	147	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → Ord 𝑐)
203		ordelsuc 7795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
204	201, 202, 203	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
205		peano2 7866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
206	38, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207		nnord 7850	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (suc 𝑛 ∈ ω → Ord suc 𝑛)
208	206, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord suc 𝑛)
209	208	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → Ord suc 𝑛)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord suc 𝑛)
211		ordtri1 6365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord suc 𝑛 ∧ Ord 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
212	210, 202, 211	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
213	204, 212	bitrd 279	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
214	200, 213	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ¬ 𝑐 ∈ suc 𝑛)
215	214	iffalsed 4499	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216		riotacl 7361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217	189, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218		nnasuc 8570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
219	162, 217, 218	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
220		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
221		nfriota1 7351	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
222		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞𝑛
223		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞 +o
224	222, 223, 221	nfov 7417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225	224	nfeq1 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227	226	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228	221, 225, 227	riota2f 7368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
229	217, 189, 228	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
230	220, 229	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐)
231		suceq 6400	. . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐)
234		peano2 7866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235	217, 234	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
236		peano2 7866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ω → suc 𝑝 ∈ ω)
237		nnasuc 8570	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
238	177, 237	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240	239	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)))
241	240	rspcev 3588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((suc 𝑝 ∈ ω ∧ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
242	236, 238, 241	syl2an2 686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
243		suceq 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244	243	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245	244	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 +o 𝑝) = 𝑐 → (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
246	242, 245	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ((𝑛 +o 𝑝) = 𝑐 → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
247	246	rexlimdva 3134	. . . . . . . . . . . . . . . . . . . . . . 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 8627	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250	177, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251		reu5 3356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252	248, 250, 251	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253	221	nfsuc 6406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞 suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254	222, 223, 253	nfov 7417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255	254	nfeq1 2907	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257	256	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258	253, 255, 257	riota2f 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
259	235, 252, 258	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
260	233, 259	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
261	260	fveq2d 6862	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262	199, 215, 261	3brtr4d 5139	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
263	262	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
264		fveq2 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘𝑏) = (𝑔‘∅))
265		suceq 6400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅)
266	265, 59	eqtr4di 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ∅ → suc 𝑏 = 1o)
267	266	fveq2d 6862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268	264, 267	breq12d 5120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ∅ → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269		eldif 3924	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270		nnord 7850	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ω → Ord 𝑚)
271		ordtri1 6365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 1o ∧ Ord 𝑚) → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
272	8, 270, 271	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ ω → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
273	272	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o) → 1o ⊆ 𝑚)
274	269, 273	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (ω ∖ 1o) → 1o ⊆ 𝑚)
275	274	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑚)
276	59, 275	eqsstrrid 3986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277		0ex 5262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ∈ V
278	113, 270	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279		ordelsuc 7795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ V ∧ Ord 𝑚) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
280	277, 278, 279	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
281	276, 280	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ 𝑚)
282	281	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∅ ∈ 𝑚)
283	268, 156, 282	rspcdva 3589	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘∅)𝑅(𝑔‘1o))
284		simpl2r 1228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = 𝑧)
285		simpr2l 1233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑔‘∅) = 𝑧)
286	284, 285	eqtr4d 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = (𝑔‘∅))
287	286	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛) = (𝑔‘∅))
288		nnon 7848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
289	38, 288	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290		oa1suc 8495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291	289, 290	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292		1onn 8604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o ∈ ω
293		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294	293	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛))
295	294	rspcev 3588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
296	292, 291, 295	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
297		nnasmo 8627	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
298	38, 297	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299		reu5 3356	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300	296, 298, 299	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301	294	riota2 7369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1o ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
302	292, 300, 301	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
303	291, 302	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
304	303	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o)
305	304	fveq2d 6862	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306	283, 287, 305	3brtr4d 5139	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307	201	sucid 6416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ suc 𝑛
308	307	iftruei 4495	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑛)
309		eleq1 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
310		fveq2 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = (𝑓‘𝑐))
311	309, 310	ifbieq1d 4513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312	308, 311	eqtr3id 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313		suceq 6400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314	313	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315	314	riotabidv 7346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316	315	fveq2d 6862	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317	312, 316	breq12d 5120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑐 → ((𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) ↔ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
318	306, 317	syl5ibcom 245	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
319	318	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
320	263, 319	jaod 859	. . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
323	135	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
324	323	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
325	324	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 ↔ ¬ suc 𝑐 ∈ suc 𝑛))
326	325	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → ¬ suc 𝑐 ∈ suc 𝑛)
327	326	iffalsed 4499	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328	322, 327	breqtrrd 5135	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329	140, 328	pm2.61dan 812	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
330		elelsuc 6407	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚))
331	330	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚))
332		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
333		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑓‘𝑝) = (𝑓‘𝑐))
334		eqeq2 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐))
335	334	riotabidv 7346	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336	335	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337	332, 333, 336	ifbieq12d 4517	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑐) ∈ V
339		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340	338, 339	ifex 4539	. . . . . . . . . . . . 13 ⊢ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V
341	337, 32, 340	fvmpt 6968	. . . . . . . . . . . 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 7797	. . . . . . . . . . . . . . 15 ⊢ (Ord (𝑛 +o 𝑚) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
344	19, 343	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
345	344	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑐 ∈ (𝑛 +o 𝑚) ↔ suc 𝑐 ∈ suc (𝑛 +o 𝑚)))
346	345	biimpa 476	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → suc 𝑐 ∈ suc (𝑛 +o 𝑚))
347		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑓‘𝑝) = (𝑓‘suc 𝑐))
349		eqeq2 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350	349	riotabidv 7346	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = suc 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351	350	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352	347, 348, 351	ifbieq12d 4517	. . . . . . . . . . . . 13 ⊢ (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
353		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑓‘suc 𝑐) ∈ V
354		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V
355	353, 354	ifex 4539	. . . . . . . . . . . . 13 ⊢ if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V
356	352, 32, 355	fvmpt 6968	. . . . . . . . . . . 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 5139	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
359	358	ralrimiva 3125	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
360		fvex 6871	. . . . . . . . . . . 12 ⊢ (𝑓‘𝑝) ∈ V
361		fvex 6871	. . . . . . . . . . . 12 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V
362	360, 361	ifex 4539	. . . . . . . . . . 11 ⊢ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363	362, 32	fnmpti 6661	. . . . . . . . . 10 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
364	46	sucex 7782	. . . . . . . . . . . 12 ⊢ suc (𝑛 +o 𝑚) ∈ V
365	364	mptex 7197	. . . . . . . . . . 11 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V
366		fneq1 6609	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)))
367		fveq1 6857	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘∅) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅))
368	367	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘∅) = 𝑥 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥))
369		fveq1 6857	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘(𝑛 +o 𝑚)) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)))
370	369	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘(𝑛 +o 𝑚)) = 𝑦 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦))
371	368, 370	anbi12d 632	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)))
372		fveq1 6857	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐))
373		fveq1 6857	. . . . . . . . . . . . . 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 3156	. . . . . . . . . . . 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 1438	. . . . . . . . . . 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 3572	. . . . . . . . . 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 1450	. . . . . . . . 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 837	. . . . . . . 8 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
380		suceq 6400	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381	380	fneq2d 6612	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (ℎ Fn suc 𝑝 ↔ ℎ Fn suc (𝑛 +o 𝑚)))
382		fveqeq2 6867	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ‘𝑝) = 𝑦 ↔ (ℎ‘(𝑛 +o 𝑚)) = 𝑦))
383	382	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ↔ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦)))
384		raleq 3296	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
385	381, 383, 384	3anbi123d 1438	. . . . . . . . . 10 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ (ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
386	385	exbidv 1921	. . . . . . . . 9 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
387	386	rspcev 3588	. . . . . . . 8 ⊢ (((𝑛 +o 𝑚) ∈ (ω ∖ 1o) ∧ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
388	23, 379, 387	syl2an2r 685	. . . . . . 7 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
389	388	ex 412	. . . . . 6 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
390	389	exlimdvv 1934	. . . . 5 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
391	390	rexlimivv 3179	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
392	391	exlimiv 1930	. . 3 ⊢ (∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
393		vex 3451	. . . . 5 ⊢ 𝑥 ∈ V
394		vex 3451	. . . . 5 ⊢ 𝑦 ∈ V
395	393, 394	opelco 5835	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦))
396		reeanv 3209	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
397		eeanv 2347	. . . . . . 7 ⊢ (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
398	397	2rexbii 3109	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
399		brttrcl 9666	. . . . . . 7 ⊢ (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
400		brttrcl 9666	. . . . . . 7 ⊢ (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
401	399, 400	anbi12i 628	. . . . . 6 ⊢ ((𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
402	396, 398, 401	3bitr4ri 304	. . . . 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 275	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
405		df-br 5108	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406		brttrcl 9666	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
407	405, 406	bitr3i 277	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 ↔ ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
408	392, 404, 407	3imtr4i 292	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
409	1, 408	relssi 5750	1 ⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  ∃!wreu 3352  ∃*wrmo 3353  Vcvv 3447   ∖ cdif 3911   ⊆ wss 3914  ∅c0 4296  ifcif 4488  ⟨cop 4595   class class class wbr 5107   ↦ cmpt 5188   ∘ ccom 5642  Ord word 6331  Oncon0 6332  suc csuc 6334   Fn wfn 6506  ‘cfv 6511  ℩crio 7343  (class class class)co 7387  ωcom 7842  1_oc1o 8427   +_o coa 8431  t++cttrcl 9660

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-oadd 8438  df-ttrcl 9661

This theorem is referenced by:  ttrclco  9671  cottrcl  9672  dfttrcl2  9677  frmin  9702  frrlem16  9711