This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ttrcltr

Description: The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024)

Ref Expression
Assertion ttrcltr ( t++ 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅

Proof

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