Theorem ttrcltr 9707

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 6097	. 2 ⊢ Rel (t++𝑅 ∘ t++𝑅)
2		eldifi 4118	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ω ∖ 1o) → 𝑛 ∈ ω)
3		eldifi 4118	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ω ∖ 1o) → 𝑚 ∈ ω)
4		nnacl 8606	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 +o 𝑚) ∈ ω)
5	2, 3, 4	syl2an 595	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ ω)
6		eldif 3950	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ (𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o))
7		1on 8473	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
8	7	onordi 6465	. . . . . . . . . . . . . . 15 ⊢ Ord 1o
9		nnord 7856	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → Ord 𝑛)
10		ordtri1 6387	. . . . . . . . . . . . . . 15 ⊢ ((Ord 1o ∧ Ord 𝑛) → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
11	8, 9, 10	sylancr 586	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o))
12	11	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o) → 1o ⊆ 𝑛)
13	6, 12	sylbi 216	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → 1o ⊆ 𝑛)
14	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑛)
15		nnaword1 8624	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → 𝑛 ⊆ (𝑛 +o 𝑚))
16	2, 3, 15	syl2an 595	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ⊆ (𝑛 +o 𝑚))
17	14, 16	sstrd 3984	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ (𝑛 +o 𝑚))
18		nnord 7856	. . . . . . . . . . . 12 ⊢ ((𝑛 +o 𝑚) ∈ ω → Ord (𝑛 +o 𝑚))
19	5, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord (𝑛 +o 𝑚))
20		ordtri1 6387	. . . . . . . . . . 11 ⊢ ((Ord 1o ∧ Ord (𝑛 +o 𝑚)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
21	8, 19, 20	sylancr 586	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (1o ⊆ (𝑛 +o 𝑚) ↔ ¬ (𝑛 +o 𝑚) ∈ 1o))
22	17, 21	mpbid 231	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ 1o)
23	5, 22	eldifd 3951	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 𝑚) ∈ (ω ∖ 1o))
24		0elsuc 7816	. . . . . . . . . . . . 13 ⊢ (Ord (𝑛 +o 𝑚) → ∅ ∈ suc (𝑛 +o 𝑚))
25	19, 24	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc (𝑛 +o 𝑚))
26		eleq1 2813	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑝 ∈ suc 𝑛 ↔ ∅ ∈ suc 𝑛))
27		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑓‘𝑝) = (𝑓‘∅))
28		eqeq2 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ∅ → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = ∅))
29	28	riotabidv 7359	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ∅ → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))
30	29	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ∅ → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)))
31	26, 27, 30	ifbieq12d 4548	. . . . . . . . . . . . 13 ⊢ (𝑝 = ∅ → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))))
32		eqid 2724	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))
33		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑓‘∅) ∈ V
34		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅)) ∈ V
35	33, 34	ifex 4570	. . . . . . . . . . . . 13 ⊢ if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) ∈ V
36	31, 32, 35	fvmpt 6988	. . . . . . . . . . . 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 7816	. . . . . . . . . . . . 13 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
41	39, 40	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∅ ∈ suc 𝑛)
42	41	iftrued 4528	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → if(∅ ∈ suc 𝑛, (𝑓‘∅), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = ∅))) = (𝑓‘∅))
43	37, 42	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = (𝑓‘∅))
44		simpl2l 1223	. . . . . . . . . 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 7434	. . . . . . . . . . . . 13 ⊢ (𝑛 +o 𝑚) ∈ V
47	46	sucid 6436	. . . . . . . . . . . 12 ⊢ (𝑛 +o 𝑚) ∈ suc (𝑛 +o 𝑚)
48		eleq1 2813	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑝 ∈ suc 𝑛 ↔ (𝑛 +o 𝑚) ∈ suc 𝑛))
49		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑓‘𝑝) = (𝑓‘(𝑛 +o 𝑚)))
50		eqeq2 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
51	50	riotabidv 7359	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑛 +o 𝑚) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))
52	51	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑛 +o 𝑚) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))))
53	48, 49, 52	ifbieq12d 4548	. . . . . . . . . . . . 13 ⊢ (𝑝 = (𝑛 +o 𝑚) → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))))
54		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑓‘(𝑛 +o 𝑚)) ∈ V
55		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) ∈ V
56	54, 55	ifex 4570	. . . . . . . . . . . . 13 ⊢ if((𝑛 +o 𝑚) ∈ suc 𝑛, (𝑓‘(𝑛 +o 𝑚)), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)))) ∈ V
57	53, 32, 56	fvmpt 6988	. . . . . . . . . . . 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 8461	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
60	59	difeq2i 4111	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
61	60	eleq2i 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
62		peano1 7872	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ ω
63		eldifsucnn 8659	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
65		dif0 4364	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∖ ∅) = ω
66	65	rexeqi 3316	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
67	61, 64, 66	3bitri 297	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
68	60	eleq2i 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ 𝑚 ∈ (ω ∖ suc ∅))
69		eldifsucnn 8659	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦))
70	62, 69	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ω ∖ suc ∅) ↔ ∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦)
71	65	rexeqi 3316	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ (ω ∖ ∅)𝑚 = suc 𝑦 ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
72	68, 70, 71	3bitri 297	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ ∃𝑦 ∈ ω 𝑚 = suc 𝑦)
73	67, 72	anbi12i 626	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
74		reeanv 3218	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) ↔ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 ∧ ∃𝑦 ∈ ω 𝑚 = suc 𝑦))
75	73, 74	bitr4i 278	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ↔ ∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦))
76		peano2 7874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ω → suc 𝑥 ∈ ω)
77		nnaword1 8624	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
78	76, 77	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ⊆ (suc 𝑥 +o 𝑦))
79	76	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc 𝑥 ∈ ω)
80		nnord 7856	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑥 ∈ ω → Ord suc 𝑥)
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc 𝑥)
82		nnacl 8606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
83	76, 82	sylan 579	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o 𝑦) ∈ ω)
84		nnord 7856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑥 +o 𝑦) ∈ ω → Ord (suc 𝑥 +o 𝑦))
85	83, 84	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o 𝑦))
86		ordsucsssuc 7804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord suc 𝑥 ∧ Ord (suc 𝑥 +o 𝑦)) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
87	81, 85, 86	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 ⊆ (suc 𝑥 +o 𝑦) ↔ suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦)))
88	78, 87	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ suc (suc 𝑥 +o 𝑦))
89		nnasuc 8601	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
90	76, 89	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) = suc (suc 𝑥 +o 𝑦))
91	88, 90	sseqtrrd 4015	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦))
92		peano2 7874	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑥 ∈ ω → suc suc 𝑥 ∈ ω)
93	79, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → suc suc 𝑥 ∈ ω)
94		nnord 7856	. . . . . . . . . . . . . . . . . 18 ⊢ (suc suc 𝑥 ∈ ω → Ord suc suc 𝑥)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord suc suc 𝑥)
96		peano2 7874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
97		nnacl 8606	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑥 ∈ ω ∧ suc 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
98	76, 96, 97	syl2an 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc 𝑥 +o suc 𝑦) ∈ ω)
99		nnord 7856	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 +o suc 𝑦) ∈ ω → Ord (suc 𝑥 +o suc 𝑦))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → Ord (suc 𝑥 +o suc 𝑦))
101		ordtri1 6387	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord suc suc 𝑥 ∧ Ord (suc 𝑥 +o suc 𝑦)) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
102	95, 100, 101	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (suc suc 𝑥 ⊆ (suc 𝑥 +o suc 𝑦) ↔ ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥))
103	91, 102	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ¬ (suc 𝑥 +o suc 𝑦) ∈ suc suc 𝑥)
104		oveq12 7410	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → (𝑛 +o 𝑚) = (suc 𝑥 +o suc 𝑦))
105		suceq 6420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = suc 𝑥 → suc 𝑛 = suc suc 𝑥)
106	105	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → suc 𝑛 = suc suc 𝑥)
107	104, 106	eleq12d 2819	. . . . . . . . . . . . . . . 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 246	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛))
110	109	rexlimivv 3191	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝑛 = suc 𝑥 ∧ 𝑚 = suc 𝑦) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
111	75, 110	sylbi 216	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ¬ (𝑛 +o 𝑚) ∈ suc 𝑛)
112	111	iffalsed 4531	. . . . . . . . . . 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 8623	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑞 ∈ ω ∧ 𝑚 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
118	114, 115, 116, 117	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ 𝑞 ∈ ω) → ((𝑛 +o 𝑞) = (𝑛 +o 𝑚) ↔ 𝑞 = 𝑚))
119	113, 118	riota5 7387	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚)) = 𝑚)
120	119	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = (𝑛 +o 𝑚))) = (𝑔‘𝑚))
121	58, 112, 120	3eqtrd 2768	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = (𝑔‘𝑚))
122		simpr2r 1230	. . . . . . . . . 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 1217	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
125		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐))
126		suceq 6420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
127	126	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
128	125, 127	breq12d 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
129	128	rspcv 3600	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑛 → (∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐)))
130	124, 129	mpan9 506	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → (𝑓‘𝑐)𝑅(𝑓‘suc 𝑐))
131		elelsuc 6427	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝑛 → 𝑐 ∈ suc 𝑛)
132	131	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → 𝑐 ∈ suc 𝑛)
133	132	iftrued 4528	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑐))
134		ordsucelsuc 7803	. . . . . . . . . . . . . . . . . 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 4528	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑓‘suc 𝑐))
139	130, 133, 138	3brtr4d 5170	. . . . . . . . . . . . 13 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
140	139	adantlr 712	. . . . . . . . . . . 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 7859	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ (𝑛 +o 𝑚) ∧ (𝑛 +o 𝑚) ∈ ω) → 𝑐 ∈ ω)
144	143	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 +o 𝑚) ∈ ω ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
145	142, 144	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ ω)
146		nnord 7856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ω → Ord 𝑐)
147	145, 146	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → Ord 𝑐)
148		ordtri3or 6386	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑛 ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
149	141, 147, 148	syl2an2r 682	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛))
150		3orel3 1481	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑐 ∈ 𝑛 → ((𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐 ∨ 𝑐 ∈ 𝑛) → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
151	149, 150	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (¬ 𝑐 ∈ 𝑛 → (𝑛 ∈ 𝑐 ∨ 𝑛 = 𝑐)))
152		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘𝑏) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
153		suceq 6420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → suc 𝑏 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
154	153	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑔‘suc 𝑏) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
155	152, 154	breq12d 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))𝑅(𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
156		simprr3 1220	. . . . . . . . . . . . . . . . . . . . 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 6370	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Ord 𝑐 ∧ 𝑛 ∈ 𝑐) → 𝑛 ⊆ 𝑐)
160	147, 159	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . 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 8632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ω ∧ 𝑐 ∈ ω) → (𝑛 ⊆ 𝑐 ↔ ∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
165	162, 163, 164	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . . . . 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 7409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o 𝑝))
168	167	eqeq1d 2726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑝 → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o 𝑝) = 𝑐))
169	168	cbvrexvw 3227	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
170	166, 169	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ ω (𝑛 +o 𝑝) = 𝑐)
171		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) = 𝑐)
172		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑐 ∈ (𝑛 +o 𝑚))
173	171, 172	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚))
174		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ (𝑝 ∈ ω ∧ (𝑛 +o 𝑝) = 𝑐)) → 𝑝 ∈ ω)
175	3	ad4antlr 730	. . . . . . . . . . . . . . . . . . . . . . . . 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 8614	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑝 ∈ 𝑚 ↔ (𝑛 +o 𝑝) ∈ (𝑛 +o 𝑚)))
180	174, 176, 178, 179	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃𝑝 ∈ 𝑚 (𝑛 +o 𝑝) = 𝑐)
183		elnn 7859	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑚 ∧ 𝑚 ∈ ω) → 𝑝 ∈ ω)
184	183	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
185	175, 184	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → 𝑝 ∈ ω)
186		nnasmo 8658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
187	177, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
188		reu5 3370	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
189	166, 187, 188	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . . . . . 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 7383	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
192	185, 190, 191	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝))
193		eqcom 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = 𝑝 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
194	192, 193	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ 𝑚) → ((𝑛 +o 𝑝) = 𝑐 ↔ 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
195	194	rexbidva 3168	. . . . . . . . . . . . . . . . . . . . 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 3222	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚 ↔ ∃𝑝 ∈ 𝑚 𝑝 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
198	196, 197	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ 𝑚)
199	155, 158, 198	rspcdva 3605	. . . . . . . . . . . . . . . . . 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 3470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑛 ∈ V
202	147	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → Ord 𝑐)
203		ordelsuc 7801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ V ∧ Ord 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
204	201, 202, 203	sylancr 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 ∈ 𝑐 ↔ suc 𝑛 ⊆ 𝑐))
205		peano2 7874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
206	38, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc 𝑛 ∈ ω)
207		nnord 7856	. . . . . . . . . . . . . . . . . . . . . . . . 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 6387	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord suc 𝑛 ∧ Ord 𝑐) → (suc 𝑛 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ suc 𝑛))
212	210, 202, 211	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ¬ 𝑐 ∈ suc 𝑛)
215	214	iffalsed 4531	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
216		riotacl 7375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
217	189, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
218		nnasuc 8601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
219	162, 217, 218	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
220		eqidd 2725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
221		nfriota1 7364	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
222		nfcv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞𝑛
223		nfcv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑞 +o
224	222, 223, 221	nfov 7431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
225	224	nfeq1 2910	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑞(𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐
226		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
227	226	eqeq1d 2726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑞 = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = 𝑐 ↔ (𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐))
228	221, 225, 227	riota2f 7382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
229	217, 189, 228	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 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 6420	. . . . . . . . . . . . . . . . . . . . . 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 7874	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
235	217, 234	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω)
236		peano2 7874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ω → suc 𝑝 ∈ ω)
237		nnasuc 8601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
238	177, 237	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝))
239		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑞 = suc 𝑝 → (𝑛 +o 𝑞) = (𝑛 +o suc 𝑝))
240	239	eqeq1d 2726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = suc 𝑝 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)))
241	240	rspcev 3604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((suc 𝑝 ∈ ω ∧ (𝑛 +o suc 𝑝) = suc (𝑛 +o 𝑝)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
242	236, 238, 241	syl2an2 683	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) ∧ 𝑝 ∈ ω) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc (𝑛 +o 𝑝))
243		suceq 6420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 +o 𝑝) = 𝑐 → suc (𝑛 +o 𝑝) = suc 𝑐)
244	243	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 +o 𝑝) = 𝑐 → ((𝑛 +o 𝑞) = suc (𝑛 +o 𝑝) ↔ (𝑛 +o 𝑞) = suc 𝑐))
245	244	rexbidv 3170	. . . . . . . . . . . . . . . . . . . . . . . . 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 3147	. . . . . . . . . . . . . . . . . . . . . . 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 8658	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
250	177, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
251		reu5 3370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
252	248, 250, 251	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)
253	221	nfsuc 6426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞 suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)
254	222, 223, 253	nfov 7431	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
255	254	nfeq1 2910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑞(𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐
256		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → (𝑛 +o 𝑞) = (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
257	256	eqeq1d 2726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) → ((𝑛 +o 𝑞) = suc 𝑐 ↔ (𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐))
258	253, 255, 257	riota2f 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐) ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) → ((𝑛 +o suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) = suc 𝑐 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐) = suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
259	235, 252, 258	syl2anc 583	. . . . . . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ 𝑛 ∈ 𝑐) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) = (𝑔‘suc (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
262	199, 215, 261	3brtr4d 5170	. . . . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘𝑏) = (𝑔‘∅))
265		suceq 6420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅)
266	265, 59	eqtr4di 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ∅ → suc 𝑏 = 1o)
267	266	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → (𝑔‘suc 𝑏) = (𝑔‘1o))
268	264, 267	breq12d 5151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ∅ → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ (𝑔‘∅)𝑅(𝑔‘1o)))
269		eldif 3950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 ∈ (ω ∖ 1o) ↔ (𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o))
270		nnord 7856	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ω → Ord 𝑚)
271		ordtri1 6387	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 1o ∧ Ord 𝑚) → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
272	8, 270, 271	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ ω → (1o ⊆ 𝑚 ↔ ¬ 𝑚 ∈ 1o))
273	272	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ ω ∧ ¬ 𝑚 ∈ 1o) → 1o ⊆ 𝑚)
274	269, 273	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (ω ∖ 1o) → 1o ⊆ 𝑚)
275	274	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 1o ⊆ 𝑚)
276	59, 275	eqsstrrid 4023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → suc ∅ ⊆ 𝑚)
277		0ex 5297	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ∈ V
278	113, 270	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → Ord 𝑚)
279		ordelsuc 7801	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ V ∧ Ord 𝑚) → (∅ ∈ 𝑚 ↔ suc ∅ ⊆ 𝑚))
280	277, 278, 279	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘∅)𝑅(𝑔‘1o))
284		simpl2r 1224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → (𝑓‘𝑛) = 𝑧)
285		simpr2l 1229	. . . . . . . . . . . . . . . . . . . . 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 7854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
289	38, 288	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → 𝑛 ∈ On)
290		oa1suc 8526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ On → (𝑛 +o 1o) = suc 𝑛)
291	289, 290	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (𝑛 +o 1o) = suc 𝑛)
292		1onn 8635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o ∈ ω
293		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 = 1o → (𝑛 +o 𝑞) = (𝑛 +o 1o))
294	293	eqeq1d 2726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑞 = 1o → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 1o) = suc 𝑛))
295	294	rspcev 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1o ∈ ω ∧ (𝑛 +o 1o) = suc 𝑛) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
296	292, 291, 295	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
297		nnasmo 8658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
298	38, 297	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
299		reu5 3370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ↔ (∃𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛 ∧ ∃*𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛))
300	296, 298, 299	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)
301	294	riota2 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1o ∈ ω ∧ ∃!𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
302	292, 300, 301	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → ((𝑛 +o 1o) = suc 𝑛 ↔ (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = 1o))
303	291, 302	mpbid 231	. . . . . . . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘1o))
306	283, 287, 305	3brtr4d 5170	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → (𝑓‘𝑛)𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)))
307	201	sucid 6436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ suc 𝑛
308	307	iftruei 4527	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = (𝑓‘𝑛)
309		eleq1 2813	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑛 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
310		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = (𝑓‘𝑐))
311	309, 310	ifbieq1d 4544	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → if(𝑛 ∈ suc 𝑛, (𝑓‘𝑛), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
312	308, 311	eqtr3id 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑓‘𝑛) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
313		suceq 6420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑐 → suc 𝑛 = suc 𝑐)
314	313	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑐 → ((𝑛 +o 𝑞) = suc 𝑛 ↔ (𝑛 +o 𝑞) = suc 𝑐))
315	314	riotabidv 7359	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
316	315	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑛)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
317	312, 316	breq12d 5151	. . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → (𝑛 = 𝑐 → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅(𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
320	263, 319	jaod 856	. . . . . . . . . . . . . . 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 4531	. . . . . . . . . . . . 13 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
328	322, 327	breqtrrd 5166	. . . . . . . . . . . 12 ⊢ (((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) ∧ ¬ 𝑐 ∈ 𝑛) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
329	140, 328	pm2.61dan 810	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))𝑅if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
330		elelsuc 6427	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝑛 +o 𝑚) → 𝑐 ∈ suc (𝑛 +o 𝑚))
331	330	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → 𝑐 ∈ suc (𝑛 +o 𝑚))
332		eleq1 2813	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑝 ∈ suc 𝑛 ↔ 𝑐 ∈ suc 𝑛))
333		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑓‘𝑝) = (𝑓‘𝑐))
334		eqeq2 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = 𝑐))
335	334	riotabidv 7359	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))
336	335	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)))
337	332, 333, 336	ifbieq12d 4548	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))))
338		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑐) ∈ V
339		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐)) ∈ V
340	338, 339	ifex 4570	. . . . . . . . . . . . 13 ⊢ if(𝑐 ∈ suc 𝑛, (𝑓‘𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑐))) ∈ V
341	337, 32, 340	fvmpt 6988	. . . . . . . . . . . 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 7803	. . . . . . . . . . . . . . 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 2813	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑝 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc 𝑛))
348		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑓‘𝑝) = (𝑓‘suc 𝑐))
349		eqeq2 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = suc 𝑐 → ((𝑛 +o 𝑞) = 𝑝 ↔ (𝑛 +o 𝑞) = suc 𝑐))
350	349	riotabidv 7359	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = suc 𝑐 → (℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝) = (℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))
351	350	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑝 = suc 𝑐 → (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) = (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)))
352	347, 348, 351	ifbieq12d 4548	. . . . . . . . . . . . 13 ⊢ (𝑝 = suc 𝑐 → if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) = if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))))
353		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑓‘suc 𝑐) ∈ V
354		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐)) ∈ V
355	353, 354	ifex 4570	. . . . . . . . . . . . 13 ⊢ if(suc 𝑐 ∈ suc 𝑛, (𝑓‘suc 𝑐), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = suc 𝑐))) ∈ V
356	352, 32, 355	fvmpt 6988	. . . . . . . . . . . 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 5170	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) ∧ 𝑐 ∈ (𝑛 +o 𝑚)) → ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
359	358	ralrimiva 3138	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∀𝑐 ∈ (𝑛 +o 𝑚)((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
360		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝑓‘𝑝) ∈ V
361		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)) ∈ V
362	360, 361	ifex 4570	. . . . . . . . . . 11 ⊢ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))) ∈ V
363	362, 32	fnmpti 6683	. . . . . . . . . 10 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)
364	46	sucex 7787	. . . . . . . . . . . 12 ⊢ suc (𝑛 +o 𝑚) ∈ V
365	364	mptex 7216	. . . . . . . . . . 11 ⊢ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) ∈ V
366		fneq1 6630	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ Fn suc (𝑛 +o 𝑚) ↔ (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) Fn suc (𝑛 +o 𝑚)))
367		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘∅) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅))
368	367	eqeq1d 2726	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘∅) = 𝑥 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥))
369		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘(𝑛 +o 𝑚)) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)))
370	369	eqeq1d 2726	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘(𝑛 +o 𝑚)) = 𝑦 ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦))
371	368, 370	anbi12d 630	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ↔ (((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘∅) = 𝑥 ∧ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘(𝑛 +o 𝑚)) = 𝑦)))
372		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐))
373		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → (ℎ‘suc 𝑐) = ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐))
374	372, 373	breq12d 5151	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝)))) → ((ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘𝑐)𝑅((𝑝 ∈ suc (𝑛 +o 𝑚) ↦ if(𝑝 ∈ suc 𝑛, (𝑓‘𝑝), (𝑔‘(℩𝑞 ∈ ω (𝑛 +o 𝑞) = 𝑝))))‘suc 𝑐)))
375	374	ralbidv 3169	. . . . . . . . . . . 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 1432	. . . . . . . . . . 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 3588	. . . . . . . . . 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 1444	. . . . . . . . 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 835	. . . . . . . 8 ⊢ (((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) ∧ ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))) → ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
380		suceq 6420	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → suc 𝑝 = suc (𝑛 +o 𝑚))
381	380	fneq2d 6633	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (ℎ Fn suc 𝑝 ↔ ℎ Fn suc (𝑛 +o 𝑚)))
382		fveqeq2 6890	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ‘𝑝) = 𝑦 ↔ (ℎ‘(𝑛 +o 𝑚)) = 𝑦))
383	382	anbi2d 628	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ↔ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦)))
384		raleq 3314	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐) ↔ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
385	381, 383, 384	3anbi123d 1432	. . . . . . . . . 10 ⊢ (𝑝 = (𝑛 +o 𝑚) → ((ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ (ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
386	385	exbidv 1916	. . . . . . . . 9 ⊢ (𝑝 = (𝑛 +o 𝑚) → (∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)) ↔ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
387	386	rspcev 3604	. . . . . . . 8 ⊢ (((𝑛 +o 𝑚) ∈ (ω ∖ 1o) ∧ ∃ℎ(ℎ Fn suc (𝑛 +o 𝑚) ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘(𝑛 +o 𝑚)) = 𝑦) ∧ ∀𝑐 ∈ (𝑛 +o 𝑚)(ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
388	23, 379, 387	syl2an2r 682	. . . . . . 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 1929	. . . . 5 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ 𝑚 ∈ (ω ∖ 1o)) → (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐))))
391	390	rexlimivv 3191	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
392	391	exlimiv 1925	. . 3 ⊢ (∃𝑧∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) → ∃𝑝 ∈ (ω ∖ 1o)∃ℎ(ℎ Fn suc 𝑝 ∧ ((ℎ‘∅) = 𝑥 ∧ (ℎ‘𝑝) = 𝑦) ∧ ∀𝑐 ∈ 𝑝 (ℎ‘𝑐)𝑅(ℎ‘suc 𝑐)))
393		vex 3470	. . . . 5 ⊢ 𝑥 ∈ V
394		vex 3470	. . . . 5 ⊢ 𝑦 ∈ V
395	393, 394	opelco 5861	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (t++𝑅 ∘ t++𝑅) ↔ ∃𝑧(𝑥t++𝑅𝑧 ∧ 𝑧t++𝑅𝑦))
396		reeanv 3218	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
397		eeanv 2337	. . . . . . 7 ⊢ (∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
398	397	2rexbii 3121	. . . . . 6 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)∃𝑓∃𝑔((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ (𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))) ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑚 ∈ (ω ∖ 1o)(∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ∧ ∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
399		brttrcl 9704	. . . . . . 7 ⊢ (𝑥t++𝑅𝑧 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑧) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
400		brttrcl 9704	. . . . . . 7 ⊢ (𝑧t++𝑅𝑦 ↔ ∃𝑚 ∈ (ω ∖ 1o)∃𝑔(𝑔 Fn suc 𝑚 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘𝑚) = 𝑦) ∧ ∀𝑏 ∈ 𝑚 (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
401	399, 400	anbi12i 626	. . . . . 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 1842	. . . 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 5139	. . . 4 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
406		brttrcl 9704	. . . 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 5777	1 ⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062  ∃!wreu 3366  ∃*wrmo 3367  Vcvv 3466   ∖ cdif 3937   ⊆ wss 3940  ∅c0 4314  ifcif 4520  ⟨cop 4626   class class class wbr 5138   ↦ cmpt 5221   ∘ ccom 5670  Ord word 6353  Oncon0 6354  suc csuc 6356   Fn wfn 6528  ‘cfv 6533  ℩crio 7356  (class class class)co 7401  ωcom 7848  1_oc1o 8454   +_o coa 8458  t++cttrcl 9698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-ttrcl 9699

This theorem is referenced by:  ttrclco  9709  cottrcl  9710  dfttrcl2  9715  frmin  9740  frrlem16  9749