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 Could not format assertion : No typesetting found for |- ( t++ R o. t++ R ) C_ t++ R with typecode |-

Proof

Step Hyp Ref Expression
1 relco Could not format Rel ( t++ R o. t++ R ) : No typesetting found for |- Rel ( t++ R o. t++ R ) with typecode |-
2 eldifi nω1𝑜nω
3 eldifi mω1𝑜mω
4 nnacl nωmωn+𝑜mω
5 2 3 4 syl2an nω1𝑜mω1𝑜n+𝑜mω
6 eldif nω1𝑜nω¬n1𝑜
7 1on 1𝑜On
8 7 onordi Ord1𝑜
9 nnord nωOrdn
10 ordtri1 Ord1𝑜Ordn1𝑜n¬n1𝑜
11 8 9 10 sylancr nω1𝑜n¬n1𝑜
12 11 biimpar nω¬n1𝑜1𝑜n
13 6 12 sylbi nω1𝑜1𝑜n
14 13 adantr nω1𝑜mω1𝑜1𝑜n
15 nnaword1 nωmωnn+𝑜m
16 2 3 15 syl2an nω1𝑜mω1𝑜nn+𝑜m
17 14 16 sstrd nω1𝑜mω1𝑜1𝑜n+𝑜m
18 nnord n+𝑜mωOrdn+𝑜m
19 5 18 syl nω1𝑜mω1𝑜Ordn+𝑜m
20 ordtri1 Ord1𝑜Ordn+𝑜m1𝑜n+𝑜m¬n+𝑜m1𝑜
21 8 19 20 sylancr nω1𝑜mω1𝑜1𝑜n+𝑜m¬n+𝑜m1𝑜
22 17 21 mpbid nω1𝑜mω1𝑜¬n+𝑜m1𝑜
23 5 22 eldifd nω1𝑜mω1𝑜n+𝑜mω1𝑜
24 0elsuc Ordn+𝑜msucn+𝑜m
25 19 24 syl nω1𝑜mω1𝑜sucn+𝑜m
26 eleq1 p=psucnsucn
27 fveq2 p=fp=f
28 eqeq2 p=n+𝑜q=pn+𝑜q=
29 28 riotabidv p=ιqω|n+𝑜q=p=ιqω|n+𝑜q=
30 29 fveq2d p=gιqω|n+𝑜q=p=gιqω|n+𝑜q=
31 26 27 30 ifbieq12d p=ifpsucnfpgιqω|n+𝑜q=p=ifsucnfgιqω|n+𝑜q=
32 eqid psucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=p
33 fvex fV
34 fvex gιqω|n+𝑜q=V
35 33 34 ifex ifsucnfgιqω|n+𝑜q=V
36 31 32 35 fvmpt sucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=ifsucnfgιqω|n+𝑜q=
37 25 36 syl nω1𝑜mω1𝑜psucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=ifsucnfgιqω|n+𝑜q=
38 2 adantr nω1𝑜mω1𝑜nω
39 38 9 syl nω1𝑜mω1𝑜Ordn
40 0elsuc Ordnsucn
41 39 40 syl nω1𝑜mω1𝑜sucn
42 41 iftrued nω1𝑜mω1𝑜ifsucnfgιqω|n+𝑜q==f
43 37 42 eqtrd nω1𝑜mω1𝑜psucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=f
44 simpl2l fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbf=x
45 43 44 sylan9eq nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=x
46 ovex n+𝑜mV
47 46 sucid n+𝑜msucn+𝑜m
48 eleq1 p=n+𝑜mpsucnn+𝑜msucn
49 fveq2 p=n+𝑜mfp=fn+𝑜m
50 eqeq2 p=n+𝑜mn+𝑜q=pn+𝑜q=n+𝑜m
51 50 riotabidv p=n+𝑜mιqω|n+𝑜q=p=ιqω|n+𝑜q=n+𝑜m
52 51 fveq2d p=n+𝑜mgιqω|n+𝑜q=p=gιqω|n+𝑜q=n+𝑜m
53 48 49 52 ifbieq12d p=n+𝑜mifpsucnfpgιqω|n+𝑜q=p=ifn+𝑜msucnfn+𝑜mgιqω|n+𝑜q=n+𝑜m
54 fvex fn+𝑜mV
55 fvex gιqω|n+𝑜q=n+𝑜mV
56 54 55 ifex ifn+𝑜msucnfn+𝑜mgιqω|n+𝑜q=n+𝑜mV
57 53 32 56 fvmpt n+𝑜msucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=ifn+𝑜msucnfn+𝑜mgιqω|n+𝑜q=n+𝑜m
58 47 57 mp1i nω1𝑜mω1𝑜psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=ifn+𝑜msucnfn+𝑜mgιqω|n+𝑜q=n+𝑜m
59 df-1o 1𝑜=suc
60 59 difeq2i ω1𝑜=ωsuc
61 60 eleq2i nω1𝑜nωsuc
62 peano1 ω
63 eldifsucnn ωnωsucxωn=sucx
64 62 63 ax-mp nωsucxωn=sucx
65 dif0 ω=ω
66 65 rexeqi xωn=sucxxωn=sucx
67 61 64 66 3bitri nω1𝑜xωn=sucx
68 60 eleq2i mω1𝑜mωsuc
69 eldifsucnn ωmωsucyωm=sucy
70 62 69 ax-mp mωsucyωm=sucy
71 65 rexeqi yωm=sucyyωm=sucy
72 68 70 71 3bitri mω1𝑜yωm=sucy
73 67 72 anbi12i nω1𝑜mω1𝑜xωn=sucxyωm=sucy
74 reeanv xωyωn=sucxm=sucyxωn=sucxyωm=sucy
75 73 74 bitr4i nω1𝑜mω1𝑜xωyωn=sucxm=sucy
76 peano2 xωsucxω
77 nnaword1 sucxωyωsucxsucx+𝑜y
78 76 77 sylan xωyωsucxsucx+𝑜y
79 76 adantr xωyωsucxω
80 nnord sucxωOrdsucx
81 79 80 syl xωyωOrdsucx
82 nnacl sucxωyωsucx+𝑜yω
83 76 82 sylan xωyωsucx+𝑜yω
84 nnord sucx+𝑜yωOrdsucx+𝑜y
85 83 84 syl xωyωOrdsucx+𝑜y
86 ordsucsssuc OrdsucxOrdsucx+𝑜ysucxsucx+𝑜ysucsucxsucsucx+𝑜y
87 81 85 86 syl2anc xωyωsucxsucx+𝑜ysucsucxsucsucx+𝑜y
88 78 87 mpbid xωyωsucsucxsucsucx+𝑜y
89 nnasuc sucxωyωsucx+𝑜sucy=sucsucx+𝑜y
90 76 89 sylan xωyωsucx+𝑜sucy=sucsucx+𝑜y
91 88 90 sseqtrrd xωyωsucsucxsucx+𝑜sucy
92 peano2 sucxωsucsucxω
93 79 92 syl xωyωsucsucxω
94 nnord sucsucxωOrdsucsucx
95 93 94 syl xωyωOrdsucsucx
96 peano2 yωsucyω
97 nnacl sucxωsucyωsucx+𝑜sucyω
98 76 96 97 syl2an xωyωsucx+𝑜sucyω
99 nnord sucx+𝑜sucyωOrdsucx+𝑜sucy
100 98 99 syl xωyωOrdsucx+𝑜sucy
101 ordtri1 OrdsucsucxOrdsucx+𝑜sucysucsucxsucx+𝑜sucy¬sucx+𝑜sucysucsucx
102 95 100 101 syl2anc xωyωsucsucxsucx+𝑜sucy¬sucx+𝑜sucysucsucx
103 91 102 mpbid xωyω¬sucx+𝑜sucysucsucx
104 oveq12 n=sucxm=sucyn+𝑜m=sucx+𝑜sucy
105 suceq n=sucxsucn=sucsucx
106 105 adantr n=sucxm=sucysucn=sucsucx
107 104 106 eleq12d n=sucxm=sucyn+𝑜msucnsucx+𝑜sucysucsucx
108 107 notbid n=sucxm=sucy¬n+𝑜msucn¬sucx+𝑜sucysucsucx
109 103 108 syl5ibrcom xωyωn=sucxm=sucy¬n+𝑜msucn
110 109 rexlimivv xωyωn=sucxm=sucy¬n+𝑜msucn
111 75 110 sylbi nω1𝑜mω1𝑜¬n+𝑜msucn
112 111 iffalsed nω1𝑜mω1𝑜ifn+𝑜msucnfn+𝑜mgιqω|n+𝑜q=n+𝑜m=gιqω|n+𝑜q=n+𝑜m
113 3 adantl nω1𝑜mω1𝑜mω
114 38 adantr nω1𝑜mω1𝑜qωnω
115 simpr nω1𝑜mω1𝑜qωqω
116 113 adantr nω1𝑜mω1𝑜qωmω
117 nnacan nωqωmωn+𝑜q=n+𝑜mq=m
118 114 115 116 117 syl3anc nω1𝑜mω1𝑜qωn+𝑜q=n+𝑜mq=m
119 113 118 riota5 nω1𝑜mω1𝑜ιqω|n+𝑜q=n+𝑜m=m
120 119 fveq2d nω1𝑜mω1𝑜gιqω|n+𝑜q=n+𝑜m=gm
121 58 112 120 3eqtrd nω1𝑜mω1𝑜psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=gm
122 simpr2r fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbgm=y
123 121 122 sylan9eq nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=y
124 simprl3 nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbanfaRfsuca
125 fveq2 a=cfa=fc
126 suceq a=csuca=succ
127 126 fveq2d a=cfsuca=fsucc
128 125 127 breq12d a=cfaRfsucafcRfsucc
129 128 rspcv cnanfaRfsucafcRfsucc
130 124 129 mpan9 nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcnfcRfsucc
131 elelsuc cncsucn
132 131 adantl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcncsucn
133 132 iftrued nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcnifcsucnfcgιqω|n+𝑜q=c=fc
134 ordsucelsuc Ordncnsuccsucn
135 39 134 syl nω1𝑜mω1𝑜cnsuccsucn
136 135 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcnsuccsucn
137 136 biimpa nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcnsuccsucn
138 137 iftrued nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcnifsuccsucnfsuccgιqω|n+𝑜q=succ=fsucc
139 130 133 138 3brtr4d nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcnifcsucnfcgιqω|n+𝑜q=cRifsuccsucnfsuccgιqω|n+𝑜q=succ
140 139 adantlr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mcnifcsucnfcgιqω|n+𝑜q=cRifsuccsucnfsuccgιqω|n+𝑜q=succ
141 39 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbOrdn
142 5 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbn+𝑜mω
143 elnn cn+𝑜mn+𝑜mωcω
144 143 ancoms n+𝑜mωcn+𝑜mcω
145 142 144 sylan nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mcω
146 nnord cωOrdc
147 145 146 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mOrdc
148 ordtri3or OrdnOrdcncn=ccn
149 141 147 148 syl2an2r nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn=ccn
150 3orel3 ¬cnncn=ccnncn=c
151 149 150 syl5com nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cnncn=c
152 fveq2 b=ιqω|n+𝑜q=cgb=gιqω|n+𝑜q=c
153 suceq b=ιqω|n+𝑜q=csucb=sucιqω|n+𝑜q=c
154 153 fveq2d b=ιqω|n+𝑜q=cgsucb=gsucιqω|n+𝑜q=c
155 152 154 breq12d b=ιqω|n+𝑜q=cgbRgsucbgιqω|n+𝑜q=cRgsucιqω|n+𝑜q=c
156 simprr3 nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbbmgbRgsucb
157 156 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mbmgbRgsucb
158 157 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncbmgbRgsucb
159 ordelss Ordcncnc
160 147 159 sylan nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncnc
161 38 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbnω
162 161 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnω
163 145 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnccω
164 nnawordex nωcωncqωn+𝑜q=c
165 162 163 164 syl2an2r nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncncqωn+𝑜q=c
166 160 165 mpbid nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncqωn+𝑜q=c
167 oveq2 q=pn+𝑜q=n+𝑜p
168 167 eqeq1d q=pn+𝑜q=cn+𝑜p=c
169 168 cbvrexvw qωn+𝑜q=cpωn+𝑜p=c
170 166 169 sylib nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=c
171 simprr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cn+𝑜p=c
172 simpllr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=ccn+𝑜m
173 171 172 eqeltrd nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cn+𝑜pn+𝑜m
174 simprl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cpω
175 3 ad4antlr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncmω
176 175 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cmω
177 162 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncnω
178 177 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cnω
179 nnaord pωmωnωpmn+𝑜pn+𝑜m
180 174 176 178 179 syl3anc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cpmn+𝑜pn+𝑜m
181 173 180 mpbird nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cpm
182 170 181 171 reximssdv nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpmn+𝑜p=c
183 elnn pmmωpω
184 183 ancoms mωpmpω
185 175 184 sylan nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpmpω
186 nnasmo nω*qωn+𝑜q=c
187 177 186 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnc*qωn+𝑜q=c
188 reu5 ∃!qωn+𝑜q=cqωn+𝑜q=c*qωn+𝑜q=c
189 166 187 188 sylanbrc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnc∃!qωn+𝑜q=c
190 189 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpm∃!qωn+𝑜q=c
191 168 riota2 pω∃!qωn+𝑜q=cn+𝑜p=cιqω|n+𝑜q=c=p
192 185 190 191 syl2anc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpmn+𝑜p=cιqω|n+𝑜q=c=p
193 eqcom ιqω|n+𝑜q=c=pp=ιqω|n+𝑜q=c
194 192 193 bitrdi nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpmn+𝑜p=cp=ιqω|n+𝑜q=c
195 194 rexbidva nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpmn+𝑜p=cpmp=ιqω|n+𝑜q=c
196 182 195 mpbid nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpmp=ιqω|n+𝑜q=c
197 risset ιqω|n+𝑜q=cmpmp=ιqω|n+𝑜q=c
198 196 197 sylibr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncιqω|n+𝑜q=cm
199 155 158 198 rspcdva nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncgιqω|n+𝑜q=cRgsucιqω|n+𝑜q=c
200 simpr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncnc
201 vex nV
202 147 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncOrdc
203 ordelsuc nVOrdcncsucnc
204 201 202 203 sylancr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncncsucnc
205 peano2 nωsucnω
206 38 205 syl nω1𝑜mω1𝑜sucnω
207 nnord sucnωOrdsucn
208 206 207 syl nω1𝑜mω1𝑜Ordsucn
209 208 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbOrdsucn
210 209 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mOrdsucn
211 ordtri1 OrdsucnOrdcsucnc¬csucn
212 210 202 211 syl2an2r nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncsucnc¬csucn
213 204 212 bitrd nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncnc¬csucn
214 200 213 mpbid nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnc¬csucn
215 214 iffalsed nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncifcsucnfcgιqω|n+𝑜q=c=gιqω|n+𝑜q=c
216 riotacl ∃!qωn+𝑜q=cιqω|n+𝑜q=cω
217 189 216 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncιqω|n+𝑜q=cω
218 nnasuc nωιqω|n+𝑜q=cωn+𝑜sucιqω|n+𝑜q=c=sucn+𝑜ιqω|n+𝑜q=c
219 162 217 218 syl2an2r nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn+𝑜sucιqω|n+𝑜q=c=sucn+𝑜ιqω|n+𝑜q=c
220 eqidd nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncιqω|n+𝑜q=c=ιqω|n+𝑜q=c
221 nfriota1 _qιqω|n+𝑜q=c
222 nfcv _qn
223 nfcv _q+𝑜
224 222 223 221 nfov _qn+𝑜ιqω|n+𝑜q=c
225 224 nfeq1 qn+𝑜ιqω|n+𝑜q=c=c
226 oveq2 q=ιqω|n+𝑜q=cn+𝑜q=n+𝑜ιqω|n+𝑜q=c
227 226 eqeq1d q=ιqω|n+𝑜q=cn+𝑜q=cn+𝑜ιqω|n+𝑜q=c=c
228 221 225 227 riota2f ιqω|n+𝑜q=cω∃!qωn+𝑜q=cn+𝑜ιqω|n+𝑜q=c=cιqω|n+𝑜q=c=ιqω|n+𝑜q=c
229 217 189 228 syl2anc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn+𝑜ιqω|n+𝑜q=c=cιqω|n+𝑜q=c=ιqω|n+𝑜q=c
230 220 229 mpbird nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn+𝑜ιqω|n+𝑜q=c=c
231 suceq n+𝑜ιqω|n+𝑜q=c=csucn+𝑜ιqω|n+𝑜q=c=succ
232 230 231 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncsucn+𝑜ιqω|n+𝑜q=c=succ
233 219 232 eqtrd nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn+𝑜sucιqω|n+𝑜q=c=succ
234 peano2 ιqω|n+𝑜q=cωsucιqω|n+𝑜q=cω
235 217 234 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncsucιqω|n+𝑜q=cω
236 peano2 pωsucpω
237 nnasuc nωpωn+𝑜sucp=sucn+𝑜p
238 177 237 sylan nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜sucp=sucn+𝑜p
239 oveq2 q=sucpn+𝑜q=n+𝑜sucp
240 239 eqeq1d q=sucpn+𝑜q=sucn+𝑜pn+𝑜sucp=sucn+𝑜p
241 240 rspcev sucpωn+𝑜sucp=sucn+𝑜pqωn+𝑜q=sucn+𝑜p
242 236 238 241 syl2an2 nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωqωn+𝑜q=sucn+𝑜p
243 suceq n+𝑜p=csucn+𝑜p=succ
244 243 eqeq2d n+𝑜p=cn+𝑜q=sucn+𝑜pn+𝑜q=succ
245 244 rexbidv n+𝑜p=cqωn+𝑜q=sucn+𝑜pqωn+𝑜q=succ
246 242 245 syl5ibcom nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cqωn+𝑜q=succ
247 246 rexlimdva nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncpωn+𝑜p=cqωn+𝑜q=succ
248 170 247 mpd nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncqωn+𝑜q=succ
249 nnasmo nω*qωn+𝑜q=succ
250 177 249 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnc*qωn+𝑜q=succ
251 reu5 ∃!qωn+𝑜q=succqωn+𝑜q=succ*qωn+𝑜q=succ
252 248 250 251 sylanbrc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mnc∃!qωn+𝑜q=succ
253 221 nfsuc _qsucιqω|n+𝑜q=c
254 222 223 253 nfov _qn+𝑜sucιqω|n+𝑜q=c
255 254 nfeq1 qn+𝑜sucιqω|n+𝑜q=c=succ
256 oveq2 q=sucιqω|n+𝑜q=cn+𝑜q=n+𝑜sucιqω|n+𝑜q=c
257 256 eqeq1d q=sucιqω|n+𝑜q=cn+𝑜q=succn+𝑜sucιqω|n+𝑜q=c=succ
258 253 255 257 riota2f sucιqω|n+𝑜q=cω∃!qωn+𝑜q=succn+𝑜sucιqω|n+𝑜q=c=succιqω|n+𝑜q=succ=sucιqω|n+𝑜q=c
259 235 252 258 syl2anc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn+𝑜sucιqω|n+𝑜q=c=succιqω|n+𝑜q=succ=sucιqω|n+𝑜q=c
260 233 259 mpbid nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncιqω|n+𝑜q=succ=sucιqω|n+𝑜q=c
261 260 fveq2d nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncgιqω|n+𝑜q=succ=gsucιqω|n+𝑜q=c
262 199 215 261 3brtr4d nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
263 262 ex nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
264 fveq2 b=gb=g
265 suceq b=sucb=suc
266 265 59 eqtr4di b=sucb=1𝑜
267 266 fveq2d b=gsucb=g1𝑜
268 264 267 breq12d b=gbRgsucbgRg1𝑜
269 eldif mω1𝑜mω¬m1𝑜
270 nnord mωOrdm
271 ordtri1 Ord1𝑜Ordm1𝑜m¬m1𝑜
272 8 270 271 sylancr mω1𝑜m¬m1𝑜
273 272 biimpar mω¬m1𝑜1𝑜m
274 269 273 sylbi mω1𝑜1𝑜m
275 274 adantl nω1𝑜mω1𝑜1𝑜m
276 59 275 eqsstrrid nω1𝑜mω1𝑜sucm
277 0ex V
278 113 270 syl nω1𝑜mω1𝑜Ordm
279 ordelsuc VOrdmmsucm
280 277 278 279 sylancr nω1𝑜mω1𝑜msucm
281 276 280 mpbird nω1𝑜mω1𝑜m
282 281 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbm
283 268 156 282 rspcdva nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbgRg1𝑜
284 simpl2r fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbfn=z
285 simpr2l fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbg=z
286 284 285 eqtr4d fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbfn=g
287 286 adantl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbfn=g
288 nnon nωnOn
289 38 288 syl nω1𝑜mω1𝑜nOn
290 oa1suc nOnn+𝑜1𝑜=sucn
291 289 290 syl nω1𝑜mω1𝑜n+𝑜1𝑜=sucn
292 1onn 1𝑜ω
293 oveq2 q=1𝑜n+𝑜q=n+𝑜1𝑜
294 293 eqeq1d q=1𝑜n+𝑜q=sucnn+𝑜1𝑜=sucn
295 294 rspcev 1𝑜ωn+𝑜1𝑜=sucnqωn+𝑜q=sucn
296 292 291 295 sylancr nω1𝑜mω1𝑜qωn+𝑜q=sucn
297 nnasmo nω*qωn+𝑜q=sucn
298 38 297 syl nω1𝑜mω1𝑜*qωn+𝑜q=sucn
299 reu5 ∃!qωn+𝑜q=sucnqωn+𝑜q=sucn*qωn+𝑜q=sucn
300 296 298 299 sylanbrc nω1𝑜mω1𝑜∃!qωn+𝑜q=sucn
301 294 riota2 1𝑜ω∃!qωn+𝑜q=sucnn+𝑜1𝑜=sucnιqω|n+𝑜q=sucn=1𝑜
302 292 300 301 sylancr nω1𝑜mω1𝑜n+𝑜1𝑜=sucnιqω|n+𝑜q=sucn=1𝑜
303 291 302 mpbid nω1𝑜mω1𝑜ιqω|n+𝑜q=sucn=1𝑜
304 303 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbιqω|n+𝑜q=sucn=1𝑜
305 304 fveq2d nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbgιqω|n+𝑜q=sucn=g1𝑜
306 283 287 305 3brtr4d nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbfnRgιqω|n+𝑜q=sucn
307 201 sucid nsucn
308 307 iftruei ifnsucnfngιqω|n+𝑜q=c=fn
309 eleq1 n=cnsucncsucn
310 fveq2 n=cfn=fc
311 309 310 ifbieq1d n=cifnsucnfngιqω|n+𝑜q=c=ifcsucnfcgιqω|n+𝑜q=c
312 308 311 eqtr3id n=cfn=ifcsucnfcgιqω|n+𝑜q=c
313 suceq n=csucn=succ
314 313 eqeq2d n=cn+𝑜q=sucnn+𝑜q=succ
315 314 riotabidv n=cιqω|n+𝑜q=sucn=ιqω|n+𝑜q=succ
316 315 fveq2d n=cgιqω|n+𝑜q=sucn=gιqω|n+𝑜q=succ
317 312 316 breq12d n=cfnRgιqω|n+𝑜q=sucnifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
318 306 317 syl5ibcom nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbn=cifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
319 318 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mn=cifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
320 263 319 jaod nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mncn=cifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
321 151 320 syld nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cnifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
322 321 imp nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cnifcsucnfcgιqω|n+𝑜q=cRgιqω|n+𝑜q=succ
323 135 notbid nω1𝑜mω1𝑜¬cn¬succsucn
324 323 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucb¬cn¬succsucn
325 324 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cn¬succsucn
326 325 biimpa nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cn¬succsucn
327 326 iffalsed nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cnifsuccsucnfsuccgιqω|n+𝑜q=succ=gιqω|n+𝑜q=succ
328 322 327 breqtrrd nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜m¬cnifcsucnfcgιqω|n+𝑜q=cRifsuccsucnfsuccgιqω|n+𝑜q=succ
329 140 328 pm2.61dan nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mifcsucnfcgιqω|n+𝑜q=cRifsuccsucnfsuccgιqω|n+𝑜q=succ
330 elelsuc cn+𝑜mcsucn+𝑜m
331 330 adantl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mcsucn+𝑜m
332 eleq1 p=cpsucncsucn
333 fveq2 p=cfp=fc
334 eqeq2 p=cn+𝑜q=pn+𝑜q=c
335 334 riotabidv p=cιqω|n+𝑜q=p=ιqω|n+𝑜q=c
336 335 fveq2d p=cgιqω|n+𝑜q=p=gιqω|n+𝑜q=c
337 332 333 336 ifbieq12d p=cifpsucnfpgιqω|n+𝑜q=p=ifcsucnfcgιqω|n+𝑜q=c
338 fvex fcV
339 fvex gιqω|n+𝑜q=cV
340 338 339 ifex ifcsucnfcgιqω|n+𝑜q=cV
341 337 32 340 fvmpt csucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pc=ifcsucnfcgιqω|n+𝑜q=c
342 331 341 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pc=ifcsucnfcgιqω|n+𝑜q=c
343 ordsucelsuc Ordn+𝑜mcn+𝑜msuccsucn+𝑜m
344 19 343 syl nω1𝑜mω1𝑜cn+𝑜msuccsucn+𝑜m
345 344 adantr nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜msuccsucn+𝑜m
346 345 biimpa nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜msuccsucn+𝑜m
347 eleq1 p=succpsucnsuccsucn
348 fveq2 p=succfp=fsucc
349 eqeq2 p=succn+𝑜q=pn+𝑜q=succ
350 349 riotabidv p=succιqω|n+𝑜q=p=ιqω|n+𝑜q=succ
351 350 fveq2d p=succgιqω|n+𝑜q=p=gιqω|n+𝑜q=succ
352 347 348 351 ifbieq12d p=succifpsucnfpgιqω|n+𝑜q=p=ifsuccsucnfsuccgιqω|n+𝑜q=succ
353 fvex fsuccV
354 fvex gιqω|n+𝑜q=succV
355 353 354 ifex ifsuccsucnfsuccgιqω|n+𝑜q=succV
356 352 32 355 fvmpt succsucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc=ifsuccsucnfsuccgιqω|n+𝑜q=succ
357 346 356 syl nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc=ifsuccsucnfsuccgιqω|n+𝑜q=succ
358 329 342 357 3brtr4d nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc
359 358 ralrimiva nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbcn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc
360 fvex fpV
361 fvex gιqω|n+𝑜q=pV
362 360 361 ifex ifpsucnfpgιqω|n+𝑜q=pV
363 362 32 fnmpti psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pFnsucn+𝑜m
364 46 sucex sucn+𝑜mV
365 364 mptex psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pV
366 fneq1 h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phFnsucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pFnsucn+𝑜m
367 fveq1 h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=ph=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=p
368 367 eqeq1d h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=ph=xpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=x
369 fveq1 h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phn+𝑜m=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m
370 369 eqeq1d h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phn+𝑜m=ypsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=y
371 368 370 anbi12d h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=ph=xhn+𝑜m=ypsucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=xpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=y
372 fveq1 h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phc=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pc
373 fveq1 h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phsucc=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc
374 372 373 breq12d h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phcRhsuccpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc
375 374 ralbidv h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcn+𝑜mhcRhsucccn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc
376 366 371 375 3anbi123d h=psucn+𝑜mifpsucnfpgιqω|n+𝑜q=phFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsuccpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pFnsucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=xpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=ycn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucc
377 365 376 spcev psucn+𝑜mifpsucnfpgιqω|n+𝑜q=pFnsucn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=xpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=ycn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucchhFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsucc
378 363 377 mp3an1 psucn+𝑜mifpsucnfpgιqω|n+𝑜q=p=xpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pn+𝑜m=ycn+𝑜mpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=pcRpsucn+𝑜mifpsucnfpgιqω|n+𝑜q=psucchhFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsucc
379 45 123 359 378 syl21anc nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbhhFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsucc
380 suceq p=n+𝑜msucp=sucn+𝑜m
381 380 fneq2d p=n+𝑜mhFnsucphFnsucn+𝑜m
382 fveqeq2 p=n+𝑜mhp=yhn+𝑜m=y
383 382 anbi2d p=n+𝑜mh=xhp=yh=xhn+𝑜m=y
384 raleq p=n+𝑜mcphcRhsucccn+𝑜mhcRhsucc
385 381 383 384 3anbi123d p=n+𝑜mhFnsucph=xhp=ycphcRhsucchFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsucc
386 385 exbidv p=n+𝑜mhhFnsucph=xhp=ycphcRhsucchhFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsucc
387 386 rspcev n+𝑜mω1𝑜hhFnsucn+𝑜mh=xhn+𝑜m=ycn+𝑜mhcRhsuccpω1𝑜hhFnsucph=xhp=ycphcRhsucc
388 23 379 387 syl2an2r nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpω1𝑜hhFnsucph=xhp=ycphcRhsucc
389 388 ex nω1𝑜mω1𝑜fFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpω1𝑜hhFnsucph=xhp=ycphcRhsucc
390 389 exlimdvv nω1𝑜mω1𝑜fgfFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpω1𝑜hhFnsucph=xhp=ycphcRhsucc
391 390 rexlimivv nω1𝑜mω1𝑜fgfFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpω1𝑜hhFnsucph=xhp=ycphcRhsucc
392 391 exlimiv znω1𝑜mω1𝑜fgfFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbpω1𝑜hhFnsucph=xhp=ycphcRhsucc
393 vex xV
394 vex yV
395 393 394 opelco Could not format ( <. x , y >. e. ( t++ R o. t++ R ) <-> E. z ( x t++ R z /\ z t++ R y ) ) : No typesetting found for |- ( <. x , y >. e. ( t++ R o. t++ R ) <-> E. z ( x t++ R z /\ z t++ R y ) ) with typecode |-
396 reeanv nω1𝑜mω1𝑜ffFnsucnf=xfn=zanfaRfsucaggFnsucmg=zgm=ybmgbRgsucbnω1𝑜ffFnsucnf=xfn=zanfaRfsucamω1𝑜ggFnsucmg=zgm=ybmgbRgsucb
397 eeanv fgfFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbffFnsucnf=xfn=zanfaRfsucaggFnsucmg=zgm=ybmgbRgsucb
398 397 2rexbii nω1𝑜mω1𝑜fgfFnsucnf=xfn=zanfaRfsucagFnsucmg=zgm=ybmgbRgsucbnω1𝑜mω1𝑜ffFnsucnf=xfn=zanfaRfsucaggFnsucmg=zgm=ybmgbRgsucb
399 brttrcl Could not format ( x t++ R z <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for |- ( x t++ R z <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) with typecode |-
400 brttrcl Could not format ( z t++ R y <-> E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) : No typesetting found for |- ( z t++ R y <-> E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) with typecode |-
401 399 400 anbi12i Could not format ( ( x t++ R z /\ z t++ R y ) <-> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) : No typesetting found for |- ( ( x t++ R z /\ z t++ R y ) <-> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) with typecode |-
402 396 398 401 3bitr4ri Could not format ( ( x t++ R z /\ z t++ R y ) <-> E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) : No typesetting found for |- ( ( x t++ R z /\ z t++ R y ) <-> E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) with typecode |-
403 402 exbii Could not format ( E. z ( x t++ R z /\ z t++ R y ) <-> E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) : No typesetting found for |- ( E. z ( x t++ R z /\ z t++ R y ) <-> E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) with typecode |-
404 395 403 bitri Could not format ( <. x , y >. e. ( t++ R o. t++ R ) <-> E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) : No typesetting found for |- ( <. x , y >. e. ( t++ R o. t++ R ) <-> E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) with typecode |-
405 df-br Could not format ( x t++ R y <-> <. x , y >. e. t++ R ) : No typesetting found for |- ( x t++ R y <-> <. x , y >. e. t++ R ) with typecode |-
406 brttrcl Could not format ( x t++ R y <-> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) ) : No typesetting found for |- ( x t++ R y <-> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) ) with typecode |-
407 405 406 bitr3i Could not format ( <. x , y >. e. t++ R <-> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) ) : No typesetting found for |- ( <. x , y >. e. t++ R <-> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) ) with typecode |-
408 392 404 407 3imtr4i Could not format ( <. x , y >. e. ( t++ R o. t++ R ) -> <. x , y >. e. t++ R ) : No typesetting found for |- ( <. x , y >. e. ( t++ R o. t++ R ) -> <. x , y >. e. t++ R ) with typecode |-
409 1 408 relssi Could not format ( t++ R o. t++ R ) C_ t++ R : No typesetting found for |- ( t++ R o. t++ R ) C_ t++ R with typecode |-