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 (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	noetasuplem.2	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
Assertion	noetasuplem1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$

Step	Hyp	Ref	Expression
1		noetasuplem.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		noetasuplem.2	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
3	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
4	3	3adant3	$⊢ (A \subseteq No \land A \in V \land B \in V) \to S \in No$
5		bdayimaon	$⊢ B \in V \to suc ⋃ bday [B] \in On$
6	5	3ad2ant3	$⊢ (A \subseteq No \land A \in V \land B \in V) \to suc ⋃ bday [B] \in On$
7		1oex	$⊢ 1_{𝑜} \in V$
8	7	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
9	8	noextendseq	$⊢ (S \in No \land suc ⋃ bday [B] \in On) \to S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \in No$
10	4 6 9	syl2anc	$⊢ (A \subseteq No \land A \in V \land B \in V) \to S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \in No$
11	2 10	eqeltrid	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$

Metamath Proof Explorer