# Metamath Proof Explorer

## Theorem nosupres

Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupres.1 ${⊢}{S}=if\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y},\left(\iota {x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\right)\cup \left\{⟨\mathrm{dom}\left(\iota {x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\right),{2}_{𝑜}⟩\right\},\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)\right)$
Assertion nosupres ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {{S}↾}_{\mathrm{suc}{G}}={{U}↾}_{\mathrm{suc}{G}}$

### Proof

Step Hyp Ref Expression
1 nosupres.1 ${⊢}{S}=if\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y},\left(\iota {x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\right)\cup \left\{⟨\mathrm{dom}\left(\iota {x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\right),{2}_{𝑜}⟩\right\},\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)\right)$
2 dmres ${⊢}\mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)=\mathrm{suc}{G}\cap \mathrm{dom}{S}$
3 1 nosupno ${⊢}\left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\to {S}\in \mathrm{No}$
4 3 3ad2ant2 ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {S}\in \mathrm{No}$
5 nodmord ${⊢}{S}\in \mathrm{No}\to \mathrm{Ord}\mathrm{dom}{S}$
6 4 5 syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{Ord}\mathrm{dom}{S}$
7 dmeq ${⊢}{p}={U}\to \mathrm{dom}{p}=\mathrm{dom}{U}$
8 7 eleq2d ${⊢}{p}={U}\to \left({G}\in \mathrm{dom}{p}↔{G}\in \mathrm{dom}{U}\right)$
9 breq2 ${⊢}{p}={U}\to \left({v}{<}_{s}{p}↔{v}{<}_{s}{U}\right)$
10 9 notbid ${⊢}{p}={U}\to \left(¬{v}{<}_{s}{p}↔¬{v}{<}_{s}{U}\right)$
11 reseq1 ${⊢}{p}={U}\to {{p}↾}_{\mathrm{suc}{G}}={{U}↾}_{\mathrm{suc}{G}}$
12 11 eqeq1d ${⊢}{p}={U}\to \left({{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}↔{{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)$
13 10 12 imbi12d ${⊢}{p}={U}\to \left(\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)↔\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
14 13 ralbidv ${⊢}{p}={U}\to \left(\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)↔\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
15 8 14 anbi12d ${⊢}{p}={U}\to \left(\left({G}\in \mathrm{dom}{p}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)↔\left({G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)$
16 15 rspcev ${⊢}\left({U}\in {A}\wedge \left({G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{p}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
17 16 3impb ${⊢}\left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\to \exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{p}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
18 dmeq ${⊢}{u}={p}\to \mathrm{dom}{u}=\mathrm{dom}{p}$
19 18 eleq2d ${⊢}{u}={p}\to \left({G}\in \mathrm{dom}{u}↔{G}\in \mathrm{dom}{p}\right)$
20 breq2 ${⊢}{u}={p}\to \left({v}{<}_{s}{u}↔{v}{<}_{s}{p}\right)$
21 20 notbid ${⊢}{u}={p}\to \left(¬{v}{<}_{s}{u}↔¬{v}{<}_{s}{p}\right)$
22 reseq1 ${⊢}{u}={p}\to {{u}↾}_{\mathrm{suc}{G}}={{p}↾}_{\mathrm{suc}{G}}$
23 22 eqeq1d ${⊢}{u}={p}\to \left({{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}↔{{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)$
24 21 23 imbi12d ${⊢}{u}={p}\to \left(\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)↔\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
25 24 ralbidv ${⊢}{u}={p}\to \left(\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)↔\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
26 19 25 anbi12d ${⊢}{u}={p}\to \left(\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)↔\left({G}\in \mathrm{dom}{p}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)$
27 26 cbvrexvw ${⊢}\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)↔\exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{p}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{p}\to {{p}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
28 17 27 sylibr ${⊢}\left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\to \exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
29 eleq1 ${⊢}{y}={G}\to \left({y}\in \mathrm{dom}{u}↔{G}\in \mathrm{dom}{u}\right)$
30 suceq ${⊢}{y}={G}\to \mathrm{suc}{y}=\mathrm{suc}{G}$
31 30 reseq2d ${⊢}{y}={G}\to {{u}↾}_{\mathrm{suc}{y}}={{u}↾}_{\mathrm{suc}{G}}$
32 30 reseq2d ${⊢}{y}={G}\to {{v}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{G}}$
33 31 32 eqeq12d ${⊢}{y}={G}\to \left({{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}↔{{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)$
34 33 imbi2d ${⊢}{y}={G}\to \left(\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)↔\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
35 34 ralbidv ${⊢}{y}={G}\to \left(\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)↔\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)$
36 29 35 anbi12d ${⊢}{y}={G}\to \left(\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)↔\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)$
37 36 rexbidv ${⊢}{y}={G}\to \left(\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)$
38 37 elabg ${⊢}{G}\in \mathrm{dom}{U}\to \left({G}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)$
39 38 3ad2ant2 ${⊢}\left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\to \left({G}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)$
40 28 39 mpbird ${⊢}\left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\to {G}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}$
41 40 3ad2ant3 ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {G}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}$
42 iffalse ${⊢}¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\to if\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y},\left(\iota {x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\right)\cup \left\{⟨\mathrm{dom}\left(\iota {x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\right),{2}_{𝑜}⟩\right\},\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)\right)=\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)$
43 1 42 syl5eq ${⊢}¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\to {S}=\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)$
44 43 dmeqd ${⊢}¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\to \mathrm{dom}{S}=\mathrm{dom}\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)$
45 iotaex ${⊢}\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\in \mathrm{V}$
46 eqid ${⊢}\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)=\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)$
47 45 46 dmmpti ${⊢}\mathrm{dom}\left({g}\in \left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}⟼\left(\iota {x}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({g}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{g}}={{v}↾}_{\mathrm{suc}{g}}\right)\wedge {u}\left({g}\right)={x}\right)\right)\right)=\left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}$
48 44 47 syl6eq ${⊢}¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\to \mathrm{dom}{S}=\left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}$
49 48 3ad2ant1 ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{dom}{S}=\left\{{y}|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{dom}{u}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{u}\to {{u}↾}_{\mathrm{suc}{y}}={{v}↾}_{\mathrm{suc}{y}}\right)\right)\right\}$
50 41 49 eleqtrrd ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {G}\in \mathrm{dom}{S}$
51 ordsucss ${⊢}\mathrm{Ord}\mathrm{dom}{S}\to \left({G}\in \mathrm{dom}{S}\to \mathrm{suc}{G}\subseteq \mathrm{dom}{S}\right)$
52 6 50 51 sylc ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{suc}{G}\subseteq \mathrm{dom}{S}$
53 df-ss ${⊢}\mathrm{suc}{G}\subseteq \mathrm{dom}{S}↔\mathrm{suc}{G}\cap \mathrm{dom}{S}=\mathrm{suc}{G}$
54 52 53 sylib ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{suc}{G}\cap \mathrm{dom}{S}=\mathrm{suc}{G}$
55 2 54 syl5eq ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)=\mathrm{suc}{G}$
56 dmres ${⊢}\mathrm{dom}\left({{U}↾}_{\mathrm{suc}{G}}\right)=\mathrm{suc}{G}\cap \mathrm{dom}{U}$
57 simp2l ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {A}\subseteq \mathrm{No}$
58 simp31 ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {U}\in {A}$
59 57 58 sseldd ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {U}\in \mathrm{No}$
60 nodmord ${⊢}{U}\in \mathrm{No}\to \mathrm{Ord}\mathrm{dom}{U}$
61 59 60 syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{Ord}\mathrm{dom}{U}$
62 simp32 ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {G}\in \mathrm{dom}{U}$
63 ordsucss ${⊢}\mathrm{Ord}\mathrm{dom}{U}\to \left({G}\in \mathrm{dom}{U}\to \mathrm{suc}{G}\subseteq \mathrm{dom}{U}\right)$
64 61 62 63 sylc ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{suc}{G}\subseteq \mathrm{dom}{U}$
65 df-ss ${⊢}\mathrm{suc}{G}\subseteq \mathrm{dom}{U}↔\mathrm{suc}{G}\cap \mathrm{dom}{U}=\mathrm{suc}{G}$
66 64 65 sylib ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{suc}{G}\cap \mathrm{dom}{U}=\mathrm{suc}{G}$
67 56 66 syl5eq ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{dom}\left({{U}↾}_{\mathrm{suc}{G}}\right)=\mathrm{suc}{G}$
68 55 67 eqtr4d ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)=\mathrm{dom}\left({{U}↾}_{\mathrm{suc}{G}}\right)$
69 55 eleq2d ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \left({a}\in \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)↔{a}\in \mathrm{suc}{G}\right)$
70 simpl1 ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to ¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}$
71 simpl2 ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)$
72 simpl31 ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to {U}\in {A}$
73 64 sselda ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to {a}\in \mathrm{dom}{U}$
74 nodmon ${⊢}{U}\in \mathrm{No}\to \mathrm{dom}{U}\in \mathrm{On}$
75 59 74 syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{dom}{U}\in \mathrm{On}$
76 onelon ${⊢}\left(\mathrm{dom}{U}\in \mathrm{On}\wedge {G}\in \mathrm{dom}{U}\right)\to {G}\in \mathrm{On}$
77 75 62 76 syl2anc ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {G}\in \mathrm{On}$
78 eloni ${⊢}{G}\in \mathrm{On}\to \mathrm{Ord}{G}$
79 77 78 syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{Ord}{G}$
80 ordsuc ${⊢}\mathrm{Ord}{G}↔\mathrm{Ord}\mathrm{suc}{G}$
81 79 80 sylib ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{Ord}\mathrm{suc}{G}$
82 ordsucss ${⊢}\mathrm{Ord}\mathrm{suc}{G}\to \left({a}\in \mathrm{suc}{G}\to \mathrm{suc}{a}\subseteq \mathrm{suc}{G}\right)$
83 81 82 syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \left({a}\in \mathrm{suc}{G}\to \mathrm{suc}{a}\subseteq \mathrm{suc}{G}\right)$
84 83 imp ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \mathrm{suc}{a}\subseteq \mathrm{suc}{G}$
85 simpl33 ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)$
86 reseq1 ${⊢}{{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\to {\left({{U}↾}_{\mathrm{suc}{G}}\right)↾}_{\mathrm{suc}{a}}={\left({{v}↾}_{\mathrm{suc}{G}}\right)↾}_{\mathrm{suc}{a}}$
87 resabs1 ${⊢}\mathrm{suc}{a}\subseteq \mathrm{suc}{G}\to {\left({{U}↾}_{\mathrm{suc}{G}}\right)↾}_{\mathrm{suc}{a}}={{U}↾}_{\mathrm{suc}{a}}$
88 resabs1 ${⊢}\mathrm{suc}{a}\subseteq \mathrm{suc}{G}\to {\left({{v}↾}_{\mathrm{suc}{G}}\right)↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}$
89 87 88 eqeq12d ${⊢}\mathrm{suc}{a}\subseteq \mathrm{suc}{G}\to \left({\left({{U}↾}_{\mathrm{suc}{G}}\right)↾}_{\mathrm{suc}{a}}={\left({{v}↾}_{\mathrm{suc}{G}}\right)↾}_{\mathrm{suc}{a}}↔{{U}↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}\right)$
90 86 89 syl5ib ${⊢}\mathrm{suc}{a}\subseteq \mathrm{suc}{G}\to \left({{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\to {{U}↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}\right)$
91 90 imim2d ${⊢}\mathrm{suc}{a}\subseteq \mathrm{suc}{G}\to \left(\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\to \left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}\right)\right)$
92 91 ralimdv ${⊢}\mathrm{suc}{a}\subseteq \mathrm{suc}{G}\to \left(\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\to \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}\right)\right)$
93 84 85 92 sylc ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}\right)$
94 1 nosupfv ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {a}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{a}}={{v}↾}_{\mathrm{suc}{a}}\right)\right)\right)\to {S}\left({a}\right)={U}\left({a}\right)$
95 70 71 72 73 93 94 syl113anc ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to {S}\left({a}\right)={U}\left({a}\right)$
96 simpr ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to {a}\in \mathrm{suc}{G}$
97 96 fvresd ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)={S}\left({a}\right)$
98 96 fvresd ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)={U}\left({a}\right)$
99 95 97 98 3eqtr4d ${⊢}\left(\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\wedge {a}\in \mathrm{suc}{G}\right)\to \left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)=\left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)$
100 99 ex ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \left({a}\in \mathrm{suc}{G}\to \left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)=\left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)\right)$
101 69 100 sylbid ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \left({a}\in \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)\to \left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)=\left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)\right)$
102 101 ralrimiv ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \forall {a}\in \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)\phantom{\rule{.4em}{0ex}}\left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)=\left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)$
103 nofun ${⊢}{S}\in \mathrm{No}\to \mathrm{Fun}{S}$
104 funres ${⊢}\mathrm{Fun}{S}\to \mathrm{Fun}\left({{S}↾}_{\mathrm{suc}{G}}\right)$
105 4 103 104 3syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{Fun}\left({{S}↾}_{\mathrm{suc}{G}}\right)$
106 nofun ${⊢}{U}\in \mathrm{No}\to \mathrm{Fun}{U}$
107 funres ${⊢}\mathrm{Fun}{U}\to \mathrm{Fun}\left({{U}↾}_{\mathrm{suc}{G}}\right)$
108 59 106 107 3syl ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \mathrm{Fun}\left({{U}↾}_{\mathrm{suc}{G}}\right)$
109 eqfunfv ${⊢}\left(\mathrm{Fun}\left({{S}↾}_{\mathrm{suc}{G}}\right)\wedge \mathrm{Fun}\left({{U}↾}_{\mathrm{suc}{G}}\right)\right)\to \left({{S}↾}_{\mathrm{suc}{G}}={{U}↾}_{\mathrm{suc}{G}}↔\left(\mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)=\mathrm{dom}\left({{U}↾}_{\mathrm{suc}{G}}\right)\wedge \forall {a}\in \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)\phantom{\rule{.4em}{0ex}}\left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)=\left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)\right)\right)$
110 105 108 109 syl2anc ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to \left({{S}↾}_{\mathrm{suc}{G}}={{U}↾}_{\mathrm{suc}{G}}↔\left(\mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)=\mathrm{dom}\left({{U}↾}_{\mathrm{suc}{G}}\right)\wedge \forall {a}\in \mathrm{dom}\left({{S}↾}_{\mathrm{suc}{G}}\right)\phantom{\rule{.4em}{0ex}}\left({{S}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)=\left({{U}↾}_{\mathrm{suc}{G}}\right)\left({a}\right)\right)\right)$
111 68 102 110 mpbir2and ${⊢}\left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}_{s}{y}\wedge \left({A}\subseteq \mathrm{No}\wedge {A}\in \mathrm{V}\right)\wedge \left({U}\in {A}\wedge {G}\in \mathrm{dom}{U}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{v}{<}_{s}{U}\to {{U}↾}_{\mathrm{suc}{G}}={{v}↾}_{\mathrm{suc}{G}}\right)\right)\right)\to {{S}↾}_{\mathrm{suc}{G}}={{U}↾}_{\mathrm{suc}{G}}$