Metamath Proof Explorer


Theorem noetasuplem1

Description: Lemma for noeta . Establish that our final surreal really is a surreal. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Hypotheses noetasuplem.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
noetasuplem.2 Z = S suc bday B dom S × 1 𝑜
Assertion noetasuplem1 A No A V B V Z No

Proof

Step Hyp Ref Expression
1 noetasuplem.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
2 noetasuplem.2 Z = S suc bday B dom S × 1 𝑜
3 1 nosupno A No A V S No
4 3 3adant3 A No A V B V S No
5 bdayimaon B V suc bday B On
6 5 3ad2ant3 A No A V B V suc bday B On
7 1oex 1 𝑜 V
8 7 prid1 1 𝑜 1 𝑜 2 𝑜
9 8 noextendseq S No suc bday B On S suc bday B dom S × 1 𝑜 No
10 4 6 9 syl2anc A No A V B V S suc bday B dom S × 1 𝑜 No
11 2 10 eqeltrid A No A V B V Z No