nosupno

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

		Ref	Expression
	Hypothesis	nosupno.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))))$
	Assertion	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$

Proof

Step	Hyp	Ref	Expression
1		nosupno.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		elex	$⊢ A \in V \to A \in V$
3		iftrue	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to 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)))) = (ι 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_{𝑜}⟩\}$
4	3	adantr	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to 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)))) = (ι 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_{𝑜}⟩\}$
5		simprl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to A \subseteq No$
6		simpl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to \exists x \in A \forall y \in A \neg x <_{s} y$
7		nomaxmo	$⊢ A \subseteq No \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
8	7	ad2antrl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
9		reu5	$⊢ \exists! x \in A \forall y \in A \neg x <_{s} y \leftrightarrow (\exists x \in A \forall y \in A \neg x <_{s} y \land \exists^{*} x \in A \forall y \in A \neg x <_{s} y)$
10	6 8 9	sylanbrc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to \exists! x \in A \forall y \in A \neg x <_{s} y$
11		riotacl	$⊢ \exists! x \in A \forall y \in A \neg x <_{s} y \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in A$
12	10 11	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in A$
13	5 12	sseldd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No$
14		2on	$⊢ 2_{𝑜} \in On$
15	14	elexi	$⊢ 2_{𝑜} \in V$
16	15	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
17	16	noextend	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \to (ι 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_{𝑜}⟩\} \in No$
18	13 17	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to (ι 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_{𝑜}⟩\} \in No$
19	4 18	eqeltrd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to 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)))) \in No$
20		iffalse	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to 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)))) = (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)))$
21	20	adantr	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to 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)))) = (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)))$
22		funmpt	$⊢ Fun (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)))$
23	22	a1i	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to Fun (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)))$
24		iotaex	$⊢ (ι 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)) \in V$
25		eqid	$⊢ (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))) = (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)))$
26	24 25	dmmpti	$⊢ dom (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))) = \{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}))\}$
27		ssel2	$⊢ (A \subseteq No \land u \in A) \to u \in No$
28		nodmon	$⊢ u \in No \to dom u \in On$
29	27 28	syl	$⊢ (A \subseteq No \land u \in A) \to dom u \in On$
30		onss	$⊢ dom u \in On \to dom u \subseteq On$
31	29 30	syl	$⊢ (A \subseteq No \land u \in A) \to dom u \subseteq On$
32	31	sseld	$⊢ (A \subseteq No \land u \in A) \to (y \in dom u \to y \in On)$
33	32	adantrd	$⊢ (A \subseteq No \land u \in A) \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \to y \in On)$
34	33	rexlimdva	$⊢ A \subseteq No \to (\exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \to y \in On)$
35	34	abssdv	$⊢ A \subseteq No \to \{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}))\} \subseteq On$
36		simplr	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to a \in b$
37	29	adantlr	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to dom u \in On$
38		ontr1	$⊢ dom u \in On \to ((a \in b \land b \in dom u) \to a \in dom u)$
39	37 38	syl	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to ((a \in b \land b \in dom u) \to a \in dom u)$
40	36 39	mpand	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to (b \in dom u \to a \in dom u)$
41	40	adantrd	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to ((b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})) \to a \in dom u)$
42		reseq1	$⊢ {u ↾}_{suc b} = {v ↾}_{suc b} \to {({u ↾}_{suc b}) ↾}_{suc a} = {({v ↾}_{suc b}) ↾}_{suc a}$
43		onelon	$⊢ (dom u \in On \land b \in dom u) \to b \in On$
44	37 43	sylan	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to b \in On$
45		onsuc	$⊢ b \in On \to suc b \in On$
46	44 45	syl	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to suc b \in On$
47		simpllr	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to a \in b$
48		eloni	$⊢ b \in On \to Ord b$
49	44 48	syl	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to Ord b$
50		ordsucelsuc	$⊢ Ord b \to (a \in b \leftrightarrow suc a \in suc b)$
51	49 50	syl	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to (a \in b \leftrightarrow suc a \in suc b)$
52	47 51	mpbid	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to suc a \in suc b$
53		onelss	$⊢ suc b \in On \to (suc a \in suc b \to suc a \subseteq suc b)$
54	46 52 53	sylc	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to suc a \subseteq suc b$
55	54	resabs1d	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to {({u ↾}_{suc b}) ↾}_{suc a} = {u ↾}_{suc a}$
56	54	resabs1d	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to {({v ↾}_{suc b}) ↾}_{suc a} = {v ↾}_{suc a}$
57	55 56	eqeq12d	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to ({({u ↾}_{suc b}) ↾}_{suc a} = {({v ↾}_{suc b}) ↾}_{suc a} \leftrightarrow {u ↾}_{suc a} = {v ↾}_{suc a})$
58	42 57	imbitrid	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to ({u ↾}_{suc b} = {v ↾}_{suc b} \to {u ↾}_{suc a} = {v ↾}_{suc a})$
59	58	imim2d	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to ((\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b}) \to (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a}))$
60	59	ralimdv	$⊢ (((A \subseteq No \land a \in b) \land u \in A) \land b \in dom u) \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b}) \to \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a}))$
61	60	expimpd	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to ((b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})) \to \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a}))$
62	41 61	jcad	$⊢ ((A \subseteq No \land a \in b) \land u \in A) \to ((b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})) \to (a \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a})))$
63	62	reximdva	$⊢ (A \subseteq No \land a \in b) \to (\exists u \in A (b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})) \to \exists u \in A (a \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a})))$
64	63	expimpd	$⊢ A \subseteq No \to ((a \in b \land \exists u \in A (b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b}))) \to \exists u \in A (a \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a})))$
65		vex	$⊢ b \in V$
66		eleq1w	$⊢ y = b \to (y \in dom u \leftrightarrow b \in dom u)$
67		suceq	$⊢ y = b \to suc y = suc b$
68	67	reseq2d	$⊢ y = b \to {u ↾}_{suc y} = {u ↾}_{suc b}$
69	67	reseq2d	$⊢ y = b \to {v ↾}_{suc y} = {v ↾}_{suc b}$
70	68 69	eqeq12d	$⊢ y = b \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc b} = {v ↾}_{suc b})$
71	70	imbi2d	$⊢ y = b \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b}))$
72	71	ralbidv	$⊢ y = b \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b}))$
73	66 72	anbi12d	$⊢ y = b \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})))$
74	73	rexbidv	$⊢ y = b \to (\exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists u \in A (b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})))$
75	65 74	elab	$⊢ b \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}))\} \leftrightarrow \exists u \in A (b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b}))$
76	75	anbi2i	$⊢ (a \in b \land b \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}))\}) \leftrightarrow (a \in b \land \exists u \in A (b \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc b} = {v ↾}_{suc b})))$
77		vex	$⊢ a \in V$
78		eleq1w	$⊢ y = a \to (y \in dom u \leftrightarrow a \in dom u)$
79		suceq	$⊢ y = a \to suc y = suc a$
80	79	reseq2d	$⊢ y = a \to {u ↾}_{suc y} = {u ↾}_{suc a}$
81	79	reseq2d	$⊢ y = a \to {v ↾}_{suc y} = {v ↾}_{suc a}$
82	80 81	eqeq12d	$⊢ y = a \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc a} = {v ↾}_{suc a})$
83	82	imbi2d	$⊢ y = a \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a}))$
84	83	ralbidv	$⊢ y = a \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a}))$
85	78 84	anbi12d	$⊢ y = a \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (a \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a})))$
86	85	rexbidv	$⊢ y = a \to (\exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists u \in A (a \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a})))$
87	77 86	elab	$⊢ a \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}))\} \leftrightarrow \exists u \in A (a \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc a} = {v ↾}_{suc a}))$
88	64 76 87	3imtr4g	$⊢ A \subseteq No \to ((a \in b \land b \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}))\}) \to a \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}))\})$
89	88	alrimivv	$⊢ A \subseteq No \to \forall a \forall b ((a \in b \land b \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}))\}) \to a \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}))\})$
90		dftr2	$⊢ Tr \{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}))\} \leftrightarrow \forall a \forall b ((a \in b \land b \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}))\}) \to a \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}))\})$
91	89 90	sylibr	$⊢ A \subseteq No \to Tr \{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}))\}$
92		dford5	$⊢ Ord \{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}))\} \leftrightarrow (\{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}))\} \subseteq On \land Tr \{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}))\})$
93	35 91 92	sylanbrc	$⊢ A \subseteq No \to Ord \{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}))\}$
94	93	adantr	$⊢ (A \subseteq No \land A \in V) \to Ord \{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}))\}$
95		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
96		fofun	$⊢ bday : No \underset{onto}{⟶} On \to Fun bday$
97	95 96	ax-mp	$⊢ Fun bday$
98		funimaexg	$⊢ (Fun bday \land A \in V) \to bday [A] \in V$
99	97 98	mpan	$⊢ A \in V \to bday [A] \in V$
100	99	uniexd	$⊢ A \in V \to ⋃ bday [A] \in V$
101	100	adantl	$⊢ (A \subseteq No \land A \in V) \to ⋃ bday [A] \in V$
102		simpl	$⊢ (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \to y \in dom u$
103	102	reximi	$⊢ \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \to \exists u \in A y \in dom u$
104	103	ss2abi	$⊢ \{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}))\} \subseteq \{y \| \exists u \in A y \in dom u\}$
105		bdayval	$⊢ u \in No \to bday (u) = dom u$
106	27 105	syl	$⊢ (A \subseteq No \land u \in A) \to bday (u) = dom u$
107		fofn	$⊢ bday : No \underset{onto}{⟶} On \to bday Fn No$
108	95 107	ax-mp	$⊢ bday Fn No$
109		fnfvima	$⊢ (bday Fn No \land A \subseteq No \land u \in A) \to bday (u) \in bday [A]$
110	108 109	mp3an1	$⊢ (A \subseteq No \land u \in A) \to bday (u) \in bday [A]$
111	106 110	eqeltrrd	$⊢ (A \subseteq No \land u \in A) \to dom u \in bday [A]$
112		elssuni	$⊢ dom u \in bday [A] \to dom u \subseteq ⋃ bday [A]$
113	111 112	syl	$⊢ (A \subseteq No \land u \in A) \to dom u \subseteq ⋃ bday [A]$
114	113	sseld	$⊢ (A \subseteq No \land u \in A) \to (y \in dom u \to y \in ⋃ bday [A])$
115	114	rexlimdva	$⊢ A \subseteq No \to (\exists u \in A y \in dom u \to y \in ⋃ bday [A])$
116	115	abssdv	$⊢ A \subseteq No \to \{y \| \exists u \in A y \in dom u\} \subseteq ⋃ bday [A]$
117	116	adantr	$⊢ (A \subseteq No \land A \in V) \to \{y \| \exists u \in A y \in dom u\} \subseteq ⋃ bday [A]$
118	104 117	sstrid	$⊢ (A \subseteq No \land A \in V) \to \{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}))\} \subseteq ⋃ bday [A]$
119	101 118	ssexd	$⊢ (A \subseteq No \land A \in V) \to \{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}))\} \in V$
120		elong	$⊢ \{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}))\} \in V \to (\{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}))\} \in On \leftrightarrow Ord \{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}))\})$
121	119 120	syl	$⊢ (A \subseteq No \land A \in V) \to (\{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}))\} \in On \leftrightarrow Ord \{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}))\})$
122	94 121	mpbird	$⊢ (A \subseteq No \land A \in V) \to \{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}))\} \in On$
123	26 122	eqeltrid	$⊢ (A \subseteq No \land A \in V) \to dom (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))) \in On$
124	123	adantl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to dom (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))) \in On$
125	25	rnmpt	$⊢ ran (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))) = \{z \| \exists 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}))\} z = (ι 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))\}$
126		vex	$⊢ g \in V$
127		eleq1w	$⊢ y = g \to (y \in dom u \leftrightarrow g \in dom u)$
128		suceq	$⊢ y = g \to suc y = suc g$
129	128	reseq2d	$⊢ y = g \to {u ↾}_{suc y} = {u ↾}_{suc g}$
130	128	reseq2d	$⊢ y = g \to {v ↾}_{suc y} = {v ↾}_{suc g}$
131	129 130	eqeq12d	$⊢ y = g \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc g} = {v ↾}_{suc g})$
132	131	imbi2d	$⊢ y = g \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))$
133	132	ralbidv	$⊢ y = g \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))$
134	127 133	anbi12d	$⊢ y = g \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g})))$
135	134	rexbidv	$⊢ y = g \to (\exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g})))$
136	126 135	elab	$⊢ 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}))\} \leftrightarrow \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))$
137		eqid	$⊢ u (g) = u (g)$
138		fvex	$⊢ u (g) \in V$
139		eqeq2	$⊢ x = u (g) \to (u (g) = x \leftrightarrow u (g) = u (g))$
140	139	3anbi3d	$⊢ x = u (g) \to ((g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x) \leftrightarrow (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = u (g)))$
141	138 140	spcev	$⊢ (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = u (g)) \to \exists x (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)$
142	137 141	mp3an3	$⊢ (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g})) \to \exists x (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)$
143	142	reximi	$⊢ \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g})) \to \exists u \in A \exists x (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)$
144		rexcom4	$⊢ \exists u \in A \exists x (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x) \leftrightarrow \exists 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)$
145	143 144	sylib	$⊢ \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g})) \to \exists 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)$
146	145	adantl	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to \exists 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)$
147		nosupprefixmo	$⊢ A \subseteq No \to \exists^{*} 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)$
148	147	adantr	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to \exists^{*} 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)$
149		df-eu	$⊢ \exists! 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) \leftrightarrow (\exists 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) \land \exists^{*} 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))$
150	146 148 149	sylanbrc	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to \exists! 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)$
151		vex	$⊢ z \in V$
152		eqeq2	$⊢ x = z \to (u (g) = x \leftrightarrow u (g) = z)$
153	152	3anbi3d	$⊢ x = z \to ((g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x) \leftrightarrow (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))$
154	153	rexbidv	$⊢ x = z \to (\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) \leftrightarrow \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) = z))$
155	154	iota2	$⊢ (z \in V \land \exists! 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)) \to (\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) = z) \leftrightarrow (ι 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)) = z)$
156	151 155	mpan	$⊢ \exists! 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) \to (\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) = z) \leftrightarrow (ι 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)) = z)$
157	150 156	syl	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to (\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) = z) \leftrightarrow (ι 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)) = z)$
158		eqcom	$⊢ (ι 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)) = z \leftrightarrow z = (ι 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))$
159	157 158	bitrdi	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to (\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) = z) \leftrightarrow z = (ι 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)))$
160		simprr3	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to u (g) = z$
161	27	adantrr	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to u \in No$
162		norn	$⊢ u \in No \to ran u \subseteq \{1_{𝑜}, 2_{𝑜}\}$
163	161 162	syl	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to ran u \subseteq \{1_{𝑜}, 2_{𝑜}\}$
164		nofun	$⊢ u \in No \to Fun u$
165	161 164	syl	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to Fun u$
166		simprr1	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to g \in dom u$
167		fvelrn	$⊢ (Fun u \land g \in dom u) \to u (g) \in ran u$
168	165 166 167	syl2anc	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to u (g) \in ran u$
169	163 168	sseldd	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to u (g) \in \{1_{𝑜}, 2_{𝑜}\}$
170	160 169	eqeltrrd	$⊢ (A \subseteq No \land (u \in A \land (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = z))) \to z \in \{1_{𝑜}, 2_{𝑜}\}$
171	170	rexlimdvaa	$⊢ A \subseteq No \to (\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) = z) \to z \in \{1_{𝑜}, 2_{𝑜}\})$
172	171	adantr	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to (\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) = z) \to z \in \{1_{𝑜}, 2_{𝑜}\})$
173	159 172	sylbird	$⊢ (A \subseteq No \land \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}))) \to (z = (ι 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)) \to z \in \{1_{𝑜}, 2_{𝑜}\})$
174	136 173	sylan2b	$⊢ (A \subseteq No \land 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}))\}) \to (z = (ι 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)) \to z \in \{1_{𝑜}, 2_{𝑜}\})$
175	174	rexlimdva	$⊢ A \subseteq No \to (\exists 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}))\} z = (ι 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)) \to z \in \{1_{𝑜}, 2_{𝑜}\})$
176	175	abssdv	$⊢ A \subseteq No \to \{z \| \exists 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}))\} z = (ι 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))\} \subseteq \{1_{𝑜}, 2_{𝑜}\}$
177	125 176	eqsstrid	$⊢ A \subseteq No \to ran (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))) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
178	177	ad2antrl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to ran (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))) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
179		elno2	$⊢ (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))) \in No \leftrightarrow (Fun (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))) \land dom (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))) \in On \land ran (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))) \subseteq \{1_{𝑜}, 2_{𝑜}\})$
180	23 124 178 179	syl3anbrc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to (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))) \in No$
181	21 180	eqeltrd	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to 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)))) \in No$
182	19 181	pm2.61ian	$⊢ (A \subseteq No \land A \in V) \to 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)))) \in No$
183	1 182	eqeltrid	$⊢ (A \subseteq No \land A \in V) \to S \in No$
184	2 183	sylan2	$⊢ (A \subseteq No \land A \in V) \to S \in No$

Metamath Proof Explorer

Theorem nosupno

Proof