nosupbnd1

Description: Bounding law from below for the surreal supremum. Proposition 4.2 of Lipparini p. 6. (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Hypothesis	nosupbnd1.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	nosupbnd1	$⊢ (A \subseteq No \land A \in V \land U \in A) \to ({U ↾}_{dom S}) <_{s} S$

Proof

Step	Hyp	Ref	Expression
1		nosupbnd1.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		simpr3	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to U \in A$
3		nfv	$⊢ Ⅎ x (A \subseteq No \land A \in V \land U \in A)$
4		nfcv	$⊢ \underline{Ⅎ} x A$
5		nfriota1	$⊢ \underline{Ⅎ} x (ι x \in A \| \forall y \in A \neg x <_{s} y)$
6		nfcv	$⊢ \underline{Ⅎ} x <_{s}$
7		nfcv	$⊢ \underline{Ⅎ} x y$
8	5 6 7	nfbr	$⊢ Ⅎ x (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y$
9	8	nfn	$⊢ Ⅎ x \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y$
10	4 9	nfralw	$⊢ Ⅎ x \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y$
11	3 10	nfim	$⊢ Ⅎ x ((A \subseteq No \land A \in V \land U \in A) \to \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y)$
12		simpl	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to (x \in A \land \forall y \in A \neg x <_{s} y)$
13		rspe	$⊢ (x \in A \land \forall y \in A \neg x <_{s} y) \to \exists x \in A \forall y \in A \neg x <_{s} y$
14	13	adantr	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to \exists x \in A \forall y \in A \neg x <_{s} y$
15		nomaxmo	$⊢ A \subseteq No \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
16	15	3ad2ant1	$⊢ (A \subseteq No \land A \in V \land U \in A) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
17	16	adantl	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
18		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)$
19	14 17 18	sylanbrc	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to \exists! x \in A \forall y \in A \neg x <_{s} y$
20		riota1	$⊢ \exists! x \in A \forall y \in A \neg x <_{s} y \to ((x \in A \land \forall y \in A \neg x <_{s} y) \leftrightarrow (ι x \in A \| \forall y \in A \neg x <_{s} y) = x)$
21	19 20	syl	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to ((x \in A \land \forall y \in A \neg x <_{s} y) \leftrightarrow (ι x \in A \| \forall y \in A \neg x <_{s} y) = x)$
22	12 21	mpbid	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) = x$
23		simplr	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to \forall y \in A \neg x <_{s} y$
24		nfra1	$⊢ Ⅎ y \forall y \in A \neg x <_{s} y$
25		nfcv	$⊢ \underline{Ⅎ} y A$
26	24 25	nfriota	$⊢ \underline{Ⅎ} y (ι x \in A \| \forall y \in A \neg x <_{s} y)$
27		nfcv	$⊢ \underline{Ⅎ} y x$
28	26 27	nfeq	$⊢ Ⅎ y (ι x \in A \| \forall y \in A \neg x <_{s} y) = x$
29		breq1	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to ((ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y \leftrightarrow x <_{s} y)$
30	29	notbid	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to (\neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y \leftrightarrow \neg x <_{s} y)$
31	28 30	ralbid	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to (\forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y \leftrightarrow \forall y \in A \neg x <_{s} y)$
32	31	biimprd	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to (\forall y \in A \neg x <_{s} y \to \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y)$
33	22 23 32	sylc	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land U \in A)) \to \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y$
34	33	exp31	$⊢ x \in A \to (\forall y \in A \neg x <_{s} y \to ((A \subseteq No \land A \in V \land U \in A) \to \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y))$
35	11 34	rexlimi	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to ((A \subseteq No \land A \in V \land U \in A) \to \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y)$
36	35	imp	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y$
37		nfcv	$⊢ \underline{Ⅎ} y <_{s}$
38		nfcv	$⊢ \underline{Ⅎ} y U$
39	26 37 38	nfbr	$⊢ Ⅎ y (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U$
40	39	nfn	$⊢ Ⅎ y \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U$
41		breq2	$⊢ y = U \to ((ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y \leftrightarrow (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U)$
42	41	notbid	$⊢ y = U \to (\neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y \leftrightarrow \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U)$
43	40 42	rspc	$⊢ U \in A \to (\forall y \in A \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} y \to \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U)$
44	2 36 43	sylc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U$
45		simpr1	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to A \subseteq No$
46		simpl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \exists x \in A \forall y \in A \neg x <_{s} y$
47	16	adantl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
48	46 47 18	sylanbrc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \exists! x \in A \forall y \in A \neg x <_{s} y$
49		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$
50	48 49	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in A$
51	45 50	sseldd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No$
52		nofun	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \to Fun (ι x \in A \| \forall y \in A \neg x <_{s} y)$
53		funrel	$⊢ Fun (ι x \in A \| \forall y \in A \neg x <_{s} y) \to Rel (ι x \in A \| \forall y \in A \neg x <_{s} y)$
54	51 52 53	3syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to Rel (ι x \in A \| \forall y \in A \neg x <_{s} y)$
55		sssucid	$⊢ dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \subseteq suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
56		relssres	$⊢ (Rel (ι x \in A \| \forall y \in A \neg x <_{s} y) \land dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \subseteq suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)) \to {(ι x \in A \| \forall y \in A \neg x <_{s} y) ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} = (ι x \in A \| \forall y \in A \neg x <_{s} y)$
57	54 55 56	sylancl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to {(ι x \in A \| \forall y \in A \neg x <_{s} y) ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} = (ι x \in A \| \forall y \in A \neg x <_{s} y)$
58	57	breq1d	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to (({(ι x \in A \| \forall y \in A \neg x <_{s} y) ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \leftrightarrow (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}))$
59	45 2	sseldd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to U \in No$
60		nodmon	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \to dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On$
61	51 60	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On$
62		sucelon	$⊢ dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On \leftrightarrow suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On$
63	61 62	sylib	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On$
64		sltres	$⊢ ((ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \land U \in No \land suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On) \to (({(ι x \in A \| \forall y \in A \neg x <_{s} y) ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U)$
65	51 59 63 64	syl3anc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to (({(ι x \in A \| \forall y \in A \neg x <_{s} y) ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U)$
66	58 65	sylbird	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to ((ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} U)$
67	44 66	mtod	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)})$
68		noextendgt	$⊢ (ι 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) <_{s} ((ι 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_{𝑜}⟩\})$
69	51 68	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ((ι 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_{𝑜}⟩\})$
70		noreson	$⊢ (U \in No \land suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in On) \to {U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} \in No$
71	59 63 70	syl2anc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to {U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} \in No$
72		2on	$⊢ 2_{𝑜} \in On$
73	72	elexi	$⊢ 2_{𝑜} \in V$
74	73	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
75	74	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$
76	51 75	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \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$
77		sltso	$⊢ <_{s} Or No$
78		sotr2	$⊢ (<_{s} Or No \land ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} \in No \land (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \land (ι 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)) \to ((\neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \land (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ((ι 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_{𝑜}⟩\})) \to ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ((ι 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_{𝑜}⟩\}))$
79	77 78	mpan	$⊢ ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} \in No \land (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \land (ι 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) \to ((\neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \land (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ((ι 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_{𝑜}⟩\})) \to ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ((ι 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_{𝑜}⟩\}))$
80	71 51 76 79	syl3anc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to ((\neg (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) \land (ι x \in A \| \forall y \in A \neg x <_{s} y) <_{s} ((ι 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_{𝑜}⟩\})) \to ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ((ι 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_{𝑜}⟩\}))$
81	67 69 80	mp2and	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to ({U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}) <_{s} ((ι 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_{𝑜}⟩\})$
82		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_{𝑜}⟩\}$
83	1 82	eqtrid	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to S = (ι 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_{𝑜}⟩\}$
84	83	dmeqd	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = dom ((ι 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_{𝑜}⟩\})$
85	73	dmsnop	$⊢ dom \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\} = \{dom (ι x \in A \| \forall y \in A \neg x <_{s} y)\}$
86	85	uneq2i	$⊢ dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup dom \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\} = dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{dom (ι x \in A \| \forall y \in A \neg x <_{s} y)\}$
87		dmun	$⊢ dom ((ι 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_{𝑜}⟩\}) = dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup dom \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}$
88		df-suc	$⊢ suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{dom (ι x \in A \| \forall y \in A \neg x <_{s} y)\}$
89	86 87 88	3eqtr4i	$⊢ dom ((ι 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_{𝑜}⟩\}) = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
90	84 89	eqtrdi	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
91	90	adantr	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to dom S = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
92	91	reseq2d	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to {U ↾}_{dom S} = {U ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}$
93	83	adantr	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to S = (ι 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_{𝑜}⟩\}$
94	81 92 93	3brtr4d	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to ({U ↾}_{dom S}) <_{s} S$
95		simpl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
96		simpr1	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to A \subseteq No$
97		simpr2	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to A \in V$
98		simpr3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to U \in A$
99	1	nosupbnd1lem6	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land U \in A) \to ({U ↾}_{dom S}) <_{s} S$
100	95 96 97 98 99	syl121anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V \land U \in A)) \to ({U ↾}_{dom S}) <_{s} S$
101	94 100	pm2.61ian	$⊢ (A \subseteq No \land A \in V \land U \in A) \to ({U ↾}_{dom S}) <_{s} S$

Metamath Proof Explorer

Theorem nosupbnd1

Proof