Metamath Proof Explorer

Theorem noinfno

Description: The next several theorems deal with a surreal "infimum". This surreal will ultimately be shown to bound B above and bound the restriction of any surreal below. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis noinfno.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
Assertion noinfno ⊢B⊆No∧B∈V→T∈No

Proof

Step Hyp Ref Expression
1 noinfno.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
2 iftrue ⊢∃x∈B∀y∈B¬y<sx→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
3 2 adantr ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
4 simprl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→B⊆No
5 simpl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃x∈B∀y∈B¬y<sx
6 nominmo ⊢B⊆No→∃*x∈B∀y∈B¬y<sx
7 6 ad2antrl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃*x∈B∀y∈B¬y<sx
8 reu5 ⊢∃!x∈B∀y∈B¬y<sx↔∃x∈B∀y∈B¬y<sx∧∃*x∈B∀y∈B¬y<sx
9 5 7 8 sylanbrc ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃!x∈B∀y∈B¬y<sx
10 riotacl ⊢∃!x∈B∀y∈B¬y<sx→ιx∈B|∀y∈B¬y<sx∈B
11 9 10 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→ιx∈B|∀y∈B¬y<sx∈B
12 4 11 sseldd ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→ιx∈B|∀y∈B¬y<sx∈No
13 1oex ⊢1𝑜∈V
14 13 prid1 ⊢1𝑜∈1𝑜2𝑜
15 14 noextend ⊢ιx∈B|∀y∈B¬y<sx∈No→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜∈No
16 12 15 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜∈No
17 3 16 eqeltrd ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈No
18 iffalse ⊢¬∃x∈B∀y∈B¬y<sx→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
19 18 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
20 funmpt ⊢Fun⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
21 20 a1i ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→Fun⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
22 iotaex ⊢ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈V
23 eqid ⊢g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
24 22 23 dmmpti ⊢dom⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
25 simpl ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→B⊆No
26 simprl ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→u∈B
27 25 26 sseldd ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→u∈No
28 nodmon ⊢u∈No→dom⁡u∈On
29 27 28 syl ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→dom⁡u∈On
30 simprrl ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→y∈dom⁡u
31 onelon ⊢dom⁡u∈On∧y∈dom⁡u→y∈On
32 29 30 31 syl2anc ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→y∈On
33 32 rexlimdvaa ⊢B⊆No→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→y∈On
34 33 abssdv ⊢B⊆No→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⊆On
35 simplr ⊢B⊆No∧a∈b∧u∈B→a∈b
36 ssel2 ⊢B⊆No∧u∈B→u∈No
37 36 adantlr ⊢B⊆No∧a∈b∧u∈B→u∈No
38 37 28 syl ⊢B⊆No∧a∈b∧u∈B→dom⁡u∈On
39 ontr1 ⊢dom⁡u∈On→a∈b∧b∈dom⁡u→a∈dom⁡u
40 38 39 syl ⊢B⊆No∧a∈b∧u∈B→a∈b∧b∈dom⁡u→a∈dom⁡u
41 35 40 mpand ⊢B⊆No∧a∈b∧u∈B→b∈dom⁡u→a∈dom⁡u
42 41 adantrd ⊢B⊆No∧a∈b∧u∈B→b∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b→a∈dom⁡u
43 reseq1 ⊢u↾suc⁡b=v↾suc⁡b→u↾suc⁡b↾suc⁡a=v↾suc⁡b↾suc⁡a
44 onelon ⊢dom⁡u∈On∧b∈dom⁡u→b∈On
45 38 44 sylan ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→b∈On
46 onsucb ⊢b∈On↔suc⁡b∈On
47 45 46 sylib ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→suc⁡b∈On
48 simpllr ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→a∈b
49 eloni ⊢b∈On→Ord⁡b
50 45 49 syl ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→Ord⁡b
51 ordsucelsuc ⊢Ord⁡b→a∈b↔suc⁡a∈suc⁡b
52 50 51 syl ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→a∈b↔suc⁡a∈suc⁡b
53 48 52 mpbid ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→suc⁡a∈suc⁡b
54 onelss ⊢suc⁡b∈On→suc⁡a∈suc⁡b→suc⁡a⊆suc⁡b
55 47 53 54 sylc ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→suc⁡a⊆suc⁡b
56 55 resabs1d ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→u↾suc⁡b↾suc⁡a=u↾suc⁡a
57 55 resabs1d ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→v↾suc⁡b↾suc⁡a=v↾suc⁡a
58 56 57 eqeq12d ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→u↾suc⁡b↾suc⁡a=v↾suc⁡b↾suc⁡a↔u↾suc⁡a=v↾suc⁡a
59 43 58 imbitrid ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→u↾suc⁡b=v↾suc⁡b→u↾suc⁡a=v↾suc⁡a
60 59 imim2d ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→¬u<sv→u↾suc⁡b=v↾suc⁡b→¬u<sv→u↾suc⁡a=v↾suc⁡a
61 60 ralimdv ⊢B⊆No∧a∈b∧u∈B∧b∈dom⁡u→∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b→∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
62 61 expimpd ⊢B⊆No∧a∈b∧u∈B→b∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b→∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
63 42 62 jcad ⊢B⊆No∧a∈b∧u∈B→b∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b→a∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
64 63 reximdva ⊢B⊆No∧a∈b→∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b→∃u∈Ba∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
65 64 expimpd ⊢B⊆No→a∈b∧∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b→∃u∈Ba∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
66 vex ⊢b∈V
67 eleq1w ⊢y=b→y∈dom⁡u↔b∈dom⁡u
68 suceq ⊢y=b→suc⁡y=suc⁡b
69 68 reseq2d ⊢y=b→u↾suc⁡y=u↾suc⁡b
70 68 reseq2d ⊢y=b→v↾suc⁡y=v↾suc⁡b
71 69 70 eqeq12d ⊢y=b→u↾suc⁡y=v↾suc⁡y↔u↾suc⁡b=v↾suc⁡b
72 71 imbi2d ⊢y=b→¬u<sv→u↾suc⁡y=v↾suc⁡y↔¬u<sv→u↾suc⁡b=v↾suc⁡b
73 72 ralbidv ⊢y=b→∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
74 67 73 anbi12d ⊢y=b→y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔b∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
75 74 rexbidv ⊢y=b→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
76 66 75 elab ⊢b∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
77 76 anbi2i ⊢a∈b∧b∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔a∈b∧∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
78 vex ⊢a∈V
79 eleq1w ⊢y=a→y∈dom⁡u↔a∈dom⁡u
80 suceq ⊢y=a→suc⁡y=suc⁡a
81 80 reseq2d ⊢y=a→u↾suc⁡y=u↾suc⁡a
82 80 reseq2d ⊢y=a→v↾suc⁡y=v↾suc⁡a
83 81 82 eqeq12d ⊢y=a→u↾suc⁡y=v↾suc⁡y↔u↾suc⁡a=v↾suc⁡a
84 83 imbi2d ⊢y=a→¬u<sv→u↾suc⁡y=v↾suc⁡y↔¬u<sv→u↾suc⁡a=v↾suc⁡a
85 84 ralbidv ⊢y=a→∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
86 79 85 anbi12d ⊢y=a→y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔a∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
87 86 rexbidv ⊢y=a→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃u∈Ba∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
88 78 87 elab ⊢a∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃u∈Ba∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡a=v↾suc⁡a
89 65 77 88 3imtr4g ⊢B⊆No→a∈b∧b∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→a∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
90 89 alrimivv ⊢B⊆No→∀a∀ba∈b∧b∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→a∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
91 dftr2 ⊢Tr⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∀a∀ba∈b∧b∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→a∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
92 90 91 sylibr ⊢B⊆No→Tr⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
93 dford5 ⊢Ord⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⊆On∧Tr⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
94 34 92 93 sylanbrc ⊢B⊆No→Ord⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
95 94 ad2antrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→Ord⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
96 bdayfo ⊢bday:No⟶ontoOn
97 fofun ⊢bday:No⟶ontoOn→Fun⁡bday
98 96 97 ax-mp ⊢Fun⁡bday
99 funimaexg ⊢Fun⁡bday∧B∈V→bdayB∈V
100 98 99 mpan ⊢B∈V→bdayB∈V
101 100 uniexd ⊢B∈V→⋃bdayB∈V
102 101 adantl ⊢B⊆No∧B∈V→⋃bdayB∈V
103 102 adantl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→⋃bdayB∈V
104 bdayval ⊢u∈No→bday⁡u=dom⁡u
105 27 104 syl ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→bday⁡u=dom⁡u
106 fofn ⊢bday:No⟶ontoOn→bdayFnNo
107 96 106 ax-mp ⊢bdayFnNo
108 fnfvima ⊢bdayFnNo∧B⊆No∧u∈B→bday⁡u∈bdayB
109 107 108 mp3an1 ⊢B⊆No∧u∈B→bday⁡u∈bdayB
110 109 adantrr ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→bday⁡u∈bdayB
111 105 110 eqeltrrd ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→dom⁡u∈bdayB
112 elssuni ⊢dom⁡u∈bdayB→dom⁡u⊆⋃bdayB
113 111 112 syl ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→dom⁡u⊆⋃bdayB
114 113 30 sseldd ⊢B⊆No∧u∈B∧y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→y∈⋃bdayB
115 114 rexlimdvaa ⊢B⊆No→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y→y∈⋃bdayB
116 115 abssdv ⊢B⊆No→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⊆⋃bdayB
117 116 ad2antrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⊆⋃bdayB
118 103 117 ssexd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y∈V
119 elong ⊢y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y∈V→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y∈On↔Ord⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
120 118 119 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y∈On↔Ord⁡y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
121 95 120 mpbird ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y∈On
122 24 121 eqeltrid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→dom⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈On
123 23 rnmpt ⊢ran⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=z|∃g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡yz=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
124 eleq1w ⊢y=g→y∈dom⁡u↔g∈dom⁡u
125 suceq ⊢y=g→suc⁡y=suc⁡g
126 125 reseq2d ⊢y=g→u↾suc⁡y=u↾suc⁡g
127 125 reseq2d ⊢y=g→v↾suc⁡y=v↾suc⁡g
128 126 127 eqeq12d ⊢y=g→u↾suc⁡y=v↾suc⁡y↔u↾suc⁡g=v↾suc⁡g
129 128 imbi2d ⊢y=g→¬u<sv→u↾suc⁡y=v↾suc⁡y↔¬u<sv→u↾suc⁡g=v↾suc⁡g
130 129 ralbidv ⊢y=g→∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g
131 124 130 anbi12d ⊢y=g→y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g
132 131 rexbidv ⊢y=g→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g
133 132 rexab ⊢∃g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡yz=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔∃g∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧z=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
134 eqid ⊢u⁡g=u⁡g
135 fvex ⊢u⁡g∈V
136 eqeq2 ⊢x=u⁡g→u⁡g=x↔u⁡g=u⁡g
137 136 3anbi3d ⊢x=u⁡g→g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=u⁡g
138 135 137 spcev ⊢g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=u⁡g→∃xg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
139 134 138 mp3an3 ⊢g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃xg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
140 139 reximi ⊢∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃u∈B∃xg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
141 rexcom4 ⊢∃u∈B∃xg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔∃x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
142 140 141 sylib ⊢∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
143 142 adantl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
144 noinfprefixmo ⊢B⊆No→∃*x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
145 144 ad2antrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃*x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
146 145 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃*x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
147 df-eu ⊢∃!x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔∃x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∧∃*x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
148 143 146 147 sylanbrc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃!x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
149 vex ⊢z∈V
150 eqeq2 ⊢x=z→u⁡g=x↔u⁡g=z
151 150 3anbi3d ⊢x=z→g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z
152 151 rexbidv ⊢x=z→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z
153 152 iota2 ⊢z∈V∧∃!x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z↔ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=z
154 149 153 mpan ⊢∃!x∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z↔ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=z
155 148 154 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z↔ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=z
156 eqcom ⊢ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=z↔z=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
157 155 156 bitrdi ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z↔z=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
158 simprr3 ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→u⁡g=z
159 simpl ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→B⊆No
160 simprl ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→u∈B
161 159 160 sseldd ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→u∈No
162 norn ⊢u∈No→ran⁡u⊆1𝑜2𝑜
163 161 162 syl ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→ran⁡u⊆1𝑜2𝑜
164 nofun ⊢u∈No→Fun⁡u
165 161 164 syl ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→Fun⁡u
166 simprr1 ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→g∈dom⁡u
167 fvelrn ⊢Fun⁡u∧g∈dom⁡u→u⁡g∈ran⁡u
168 165 166 167 syl2anc ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→u⁡g∈ran⁡u
169 163 168 sseldd ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→u⁡g∈1𝑜2𝑜
170 158 169 eqeltrrd ⊢B⊆No∧u∈B∧g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→z∈1𝑜2𝑜
171 170 rexlimdvaa ⊢B⊆No→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→z∈1𝑜2𝑜
172 171 ad2antrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→z∈1𝑜2𝑜
173 172 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=z→z∈1𝑜2𝑜
174 157 173 sylbird ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g→z=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x→z∈1𝑜2𝑜
175 174 expimpd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧z=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x→z∈1𝑜2𝑜
176 175 exlimdv ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃g∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧z=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x→z∈1𝑜2𝑜
177 133 176 biimtrid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→∃g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡yz=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x→z∈1𝑜2𝑜
178 177 abssdv ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→z|∃g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡yz=ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x⊆1𝑜2𝑜
179 123 178 eqsstrid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→ran⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x⊆1𝑜2𝑜
180 elno2 ⊢g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈No↔Fun⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∧dom⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈On∧ran⁡g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x⊆1𝑜2𝑜
181 21 122 179 180 syl3anbrc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈No
182 19 181 eqeltrd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈No
183 17 182 pm2.61ian ⊢B⊆No∧B∈V→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x∈No
184 1 183 eqeltrid ⊢B⊆No∧B∈V→T∈No