nosupbnd2

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

		Ref	Expression
	Hypothesis	nosupbnd2.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	nosupbnd2	$⊢ (A \subseteq No \land A \in V \land Z \in No) \to (\forall a \in A a <_{s} Z \leftrightarrow \neg ({Z ↾}_{dom S}) <_{s} S)$

Proof

Step	Hyp	Ref	Expression
1		nosupbnd2.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		nfv	$⊢ Ⅎ x ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)$
3		nfcv	$⊢ \underline{Ⅎ} x Z$
4		nfre1	$⊢ Ⅎ x \exists x \in A \forall y \in A \neg x <_{s} y$
5		nfriota1	$⊢ \underline{Ⅎ} x (ι x \in A \| \forall y \in A \neg x <_{s} y)$
6	5	nfdm	$⊢ \underline{Ⅎ} x dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
7		nfcv	$⊢ \underline{Ⅎ} x 2_{𝑜}$
8	6 7	nfop	$⊢ \underline{Ⅎ} x ⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩$
9	8	nfsn	$⊢ \underline{Ⅎ} x \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}$
10	5 9	nfun	$⊢ \underline{Ⅎ} 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_{𝑜}⟩\})$
11		nfcv	$⊢ \underline{Ⅎ} 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}))\}$
12		nfiota1	$⊢ \underline{Ⅎ} x (ι 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))$
13	11 12	nfmpt	$⊢ \underline{Ⅎ} 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)))$
14	4 10 13	nfif	$⊢ \underline{Ⅎ} x 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))))$
15	1 14	nfcxfr	$⊢ \underline{Ⅎ} x S$
16	15	nfdm	$⊢ \underline{Ⅎ} x dom S$
17	3 16	nfres	$⊢ \underline{Ⅎ} x ({Z ↾}_{dom S})$
18		nfcv	$⊢ \underline{Ⅎ} x <_{s}$
19	17 18 15	nfbr	$⊢ Ⅎ x ({Z ↾}_{dom S}) <_{s} S$
20	19	nfn	$⊢ Ⅎ x \neg ({Z ↾}_{dom S}) <_{s} S$
21	2 20	nfim	$⊢ Ⅎ x (((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z) \to \neg ({Z ↾}_{dom S}) <_{s} S)$
22		simpl	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (x \in A \land \forall y \in A \neg x <_{s} y)$
23		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$
24	23	adantr	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \exists x \in A \forall y \in A \neg x <_{s} y$
25		nomaxmo	$⊢ A \subseteq No \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
26	25	3ad2ant1	$⊢ (A \subseteq No \land A \in V \land Z \in No) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
27	26	ad2antrl	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
28		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)$
29	24 27 28	sylanbrc	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \exists! x \in A \forall y \in A \neg x <_{s} y$
30		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)$
31	29 30	syl	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \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)$
32	22 31	mpbid	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) = x$
33		nosupbnd2lem1	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land (A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z) \to \neg ({Z ↾}_{suc dom x}) <_{s} (x \cup \{⟨dom x, 2_{𝑜}⟩\})$
34	33	3expb	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \neg ({Z ↾}_{suc dom x}) <_{s} (x \cup \{⟨dom x, 2_{𝑜}⟩\})$
35		dmeq	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = dom x$
36		suceq	$⊢ dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = dom x \to suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = suc dom x$
37	35 36	syl	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = suc dom x$
38	37	reseq2d	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to {Z ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)} = {Z ↾}_{suc dom x}$
39		id	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to (ι x \in A \| \forall y \in A \neg x <_{s} y) = x$
40	35	opeq1d	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to ⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩ = ⟨dom x, 2_{𝑜}⟩$
41	40	sneqd	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\} = \{⟨dom x, 2_{𝑜}⟩\}$
42	39 41	uneq12d	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \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_{𝑜}⟩\} = x \cup \{⟨dom x, 2_{𝑜}⟩\}$
43	38 42	breq12d	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to (({Z ↾}_{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_{𝑜}⟩\}) \leftrightarrow ({Z ↾}_{suc dom x}) <_{s} (x \cup \{⟨dom x, 2_{𝑜}⟩\}))$
44	43	notbid	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to (\neg ({Z ↾}_{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_{𝑜}⟩\}) \leftrightarrow \neg ({Z ↾}_{suc dom x}) <_{s} (x \cup \{⟨dom x, 2_{𝑜}⟩\}))$
45	34 44	syl5ibrcom	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to ((ι x \in A \| \forall y \in A \neg x <_{s} y) = x \to \neg ({Z ↾}_{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_{𝑜}⟩\}))$
46	32 45	mpd	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \neg ({Z ↾}_{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_{𝑜}⟩\})$
47		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_{𝑜}⟩\}$
48	1 47	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_{𝑜}⟩\}$
49	23 48	syl	$⊢ (x \in A \land \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_{𝑜}⟩\}$
50	49	dmeqd	$⊢ (x \in A \land \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_{𝑜}⟩\})$
51		2on	$⊢ 2_{𝑜} \in On$
52	51	elexi	$⊢ 2_{𝑜} \in V$
53	52	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)\}$
54	53	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)\}$
55		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_{𝑜}⟩\}$
56		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)\}$
57	54 55 56	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)$
58	50 57	eqtrdi	$⊢ (x \in A \land \forall y \in A \neg x <_{s} y) \to dom S = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
59	58	reseq2d	$⊢ (x \in A \land \forall y \in A \neg x <_{s} y) \to {Z ↾}_{dom S} = {Z ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}$
60	59	adantr	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to {Z ↾}_{dom S} = {Z ↾}_{suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)}$
61	49	adantr	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \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_{𝑜}⟩\}$
62	60 61	breq12d	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (({Z ↾}_{dom S}) <_{s} S \leftrightarrow ({Z ↾}_{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_{𝑜}⟩\}))$
63	46 62	mtbird	$⊢ ((x \in A \land \forall y \in A \neg x <_{s} y) \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \neg ({Z ↾}_{dom S}) <_{s} S$
64	63	exp31	$⊢ x \in A \to (\forall y \in A \neg x <_{s} y \to (((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z) \to \neg ({Z ↾}_{dom S}) <_{s} S))$
65	21 64	rexlimi	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to (((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z) \to \neg ({Z ↾}_{dom S}) <_{s} S)$
66	65	imp	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \neg ({Z ↾}_{dom S}) <_{s} S$
67	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
68	67	3adant3	$⊢ (A \subseteq No \land A \in V \land Z \in No) \to S \in No$
69	68	ad2antrl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to S \in No$
70		nodmon	$⊢ S \in No \to dom S \in On$
71	69 70	syl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to dom S \in On$
72		noreson	$⊢ (S \in No \land dom S \in On) \to {S ↾}_{dom S} \in No$
73	69 71 72	syl2anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to {S ↾}_{dom S} \in No$
74		simprl3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to Z \in No$
75		noreson	$⊢ (Z \in No \land dom S \in On) \to {Z ↾}_{dom S} \in No$
76	74 71 75	syl2anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to {Z ↾}_{dom S} \in No$
77		dmres	$⊢ dom ({S ↾}_{dom S}) = dom S \cap dom S$
78		inss2	$⊢ dom S \cap dom S \subseteq dom S$
79	77 78	eqsstri	$⊢ dom ({S ↾}_{dom S}) \subseteq dom S$
80	79	a1i	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to dom ({S ↾}_{dom S}) \subseteq dom S$
81		dmres	$⊢ dom ({Z ↾}_{dom S}) = dom S \cap dom Z$
82		inss1	$⊢ dom S \cap dom Z \subseteq dom S$
83	81 82	eqsstri	$⊢ dom ({Z ↾}_{dom S}) \subseteq dom S$
84	83	a1i	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to dom ({Z ↾}_{dom S}) \subseteq dom S$
85	1	nosupdm	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{g \| \exists p \in A (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g}))\}$
86	85	eqabrd	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to (g \in dom S \leftrightarrow \exists p \in A (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))$
87	86	adantr	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (g \in dom S \leftrightarrow \exists p \in A (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))$
88		simprl	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to p \in A$
89		simplrr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \forall a \in A a <_{s} Z$
90		breq1	$⊢ a = p \to (a <_{s} Z \leftrightarrow p <_{s} Z)$
91	90	rspcv	$⊢ p \in A \to (\forall a \in A a <_{s} Z \to p <_{s} Z)$
92	88 89 91	sylc	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to p <_{s} Z$
93		simprl1	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to A \subseteq No$
94	93	adantr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to A \subseteq No$
95	94 88	sseldd	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to p \in No$
96	74	adantr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to Z \in No$
97		sltso	$⊢ <_{s} Or No$
98		soasym	$⊢ (<_{s} Or No \land (p \in No \land Z \in No)) \to (p <_{s} Z \to \neg Z <_{s} p)$
99	97 98	mpan	$⊢ (p \in No \land Z \in No) \to (p <_{s} Z \to \neg Z <_{s} p)$
100	95 96 99	syl2anc	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to (p <_{s} Z \to \neg Z <_{s} p)$
101	92 100	mpd	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \neg Z <_{s} p$
102		nodmon	$⊢ p \in No \to dom p \in On$
103	95 102	syl	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to dom p \in On$
104		simprrl	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to g \in dom p$
105		onelon	$⊢ (dom p \in On \land g \in dom p) \to g \in On$
106	103 104 105	syl2anc	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to g \in On$
107		onsucb	$⊢ g \in On \leftrightarrow suc g \in On$
108	106 107	sylib	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to suc g \in On$
109		sltres	$⊢ (Z \in No \land p \in No \land suc g \in On) \to (({Z ↾}_{suc g}) <_{s} ({p ↾}_{suc g}) \to Z <_{s} p)$
110	96 95 108 109	syl3anc	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to (({Z ↾}_{suc g}) <_{s} ({p ↾}_{suc g}) \to Z <_{s} p)$
111	101 110	mtod	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \neg ({Z ↾}_{suc g}) <_{s} ({p ↾}_{suc g})$
112		simpll	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
113		simprl2	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to A \in V$
114	93 113	jca	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (A \subseteq No \land A \in V)$
115	114	adantr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to (A \subseteq No \land A \in V)$
116		simprrr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})$
117		breq1	$⊢ v = q \to (v <_{s} p \leftrightarrow q <_{s} p)$
118	117	notbid	$⊢ v = q \to (\neg v <_{s} p \leftrightarrow \neg q <_{s} p)$
119		reseq1	$⊢ v = q \to {v ↾}_{suc g} = {q ↾}_{suc g}$
120	119	eqeq2d	$⊢ v = q \to ({p ↾}_{suc g} = {v ↾}_{suc g} \leftrightarrow {p ↾}_{suc g} = {q ↾}_{suc g})$
121	118 120	imbi12d	$⊢ v = q \to ((\neg v <_{s} p \to {p ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g}))$
122	121	cbvralvw	$⊢ \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})$
123	116 122	sylibr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc g} = {v ↾}_{suc g})$
124	1	nosupres	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (p \in A \land g \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc g} = {v ↾}_{suc g}))) \to {S ↾}_{suc g} = {p ↾}_{suc g}$
125	112 115 88 104 123 124	syl113anc	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to {S ↾}_{suc g} = {p ↾}_{suc g}$
126	125	breq2d	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to (({Z ↾}_{suc g}) <_{s} ({S ↾}_{suc g}) \leftrightarrow ({Z ↾}_{suc g}) <_{s} ({p ↾}_{suc g}))$
127	111 126	mtbird	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land (p \in A \land (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})))) \to \neg ({Z ↾}_{suc g}) <_{s} ({S ↾}_{suc g})$
128	127	rexlimdvaa	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (\exists p \in A (g \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc g} = {q ↾}_{suc g})) \to \neg ({Z ↾}_{suc g}) <_{s} ({S ↾}_{suc g}))$
129	87 128	sylbid	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (g \in dom S \to \neg ({Z ↾}_{suc g}) <_{s} ({S ↾}_{suc g}))$
130	129	imp	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to \neg ({Z ↾}_{suc g}) <_{s} ({S ↾}_{suc g})$
131	69	adantr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to S \in No$
132		nodmord	$⊢ S \in No \to Ord dom S$
133	131 132	syl	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to Ord dom S$
134		simpr	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to g \in dom S$
135		ordsucss	$⊢ Ord dom S \to (g \in dom S \to suc g \subseteq dom S)$
136	133 134 135	sylc	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to suc g \subseteq dom S$
137	136	resabs1d	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to {({Z ↾}_{dom S}) ↾}_{suc g} = {Z ↾}_{suc g}$
138	136	resabs1d	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to {({S ↾}_{dom S}) ↾}_{suc g} = {S ↾}_{suc g}$
139	137 138	breq12d	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to (({({Z ↾}_{dom S}) ↾}_{suc g}) <_{s} ({({S ↾}_{dom S}) ↾}_{suc g}) \leftrightarrow ({Z ↾}_{suc g}) <_{s} ({S ↾}_{suc g}))$
140	130 139	mtbird	$⊢ ((\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \land g \in dom S) \to \neg ({({Z ↾}_{dom S}) ↾}_{suc g}) <_{s} ({({S ↾}_{dom S}) ↾}_{suc g})$
141	140	ralrimiva	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \forall g \in dom S \neg ({({Z ↾}_{dom S}) ↾}_{suc g}) <_{s} ({({S ↾}_{dom S}) ↾}_{suc g})$
142		noresle	$⊢ (({S ↾}_{dom S} \in No \land {Z ↾}_{dom S} \in No) \land (dom ({S ↾}_{dom S}) \subseteq dom S \land dom ({Z ↾}_{dom S}) \subseteq dom S \land \forall g \in dom S \neg ({({Z ↾}_{dom S}) ↾}_{suc g}) <_{s} ({({S ↾}_{dom S}) ↾}_{suc g}))) \to \neg ({Z ↾}_{dom S}) <_{s} ({S ↾}_{dom S})$
143	73 76 80 84 141 142	syl23anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \neg ({Z ↾}_{dom S}) <_{s} ({S ↾}_{dom S})$
144		nofun	$⊢ S \in No \to Fun S$
145		funrel	$⊢ Fun S \to Rel S$
146		resdm	$⊢ Rel S \to {S ↾}_{dom S} = S$
147	69 144 145 146	4syl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to {S ↾}_{dom S} = S$
148	147	breq2d	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to (({Z ↾}_{dom S}) <_{s} ({S ↾}_{dom S}) \leftrightarrow ({Z ↾}_{dom S}) <_{s} S)$
149	143 148	mtbid	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z)) \to \neg ({Z ↾}_{dom S}) <_{s} S$
150	66 149	pm2.61ian	$⊢ ((A \subseteq No \land A \in V \land Z \in No) \land \forall a \in A a <_{s} Z) \to \neg ({Z ↾}_{dom S}) <_{s} S$
151		simpll1	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to A \subseteq No$
152		simpll2	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to A \in V$
153		simpr	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to a \in A$
154	1	nosupbnd1	$⊢ (A \subseteq No \land A \in V \land a \in A) \to ({a ↾}_{dom S}) <_{s} S$
155	151 152 153 154	syl3anc	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to ({a ↾}_{dom S}) <_{s} S$
156		simplr	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to \neg ({Z ↾}_{dom S}) <_{s} S$
157		simpl1	$⊢ ((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \to A \subseteq No$
158	157	sselda	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to a \in No$
159	151 152 67	syl2anc	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to S \in No$
160	159 70	syl	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to dom S \in On$
161		noreson	$⊢ (a \in No \land dom S \in On) \to {a ↾}_{dom S} \in No$
162	158 160 161	syl2anc	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to {a ↾}_{dom S} \in No$
163		simpll3	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to Z \in No$
164	163 160 75	syl2anc	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to {Z ↾}_{dom S} \in No$
165		sotr3	$⊢ (<_{s} Or No \land ({a ↾}_{dom S} \in No \land S \in No \land {Z ↾}_{dom S} \in No)) \to ((({a ↾}_{dom S}) <_{s} S \land \neg ({Z ↾}_{dom S}) <_{s} S) \to ({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}))$
166	97 165	mpan	$⊢ ({a ↾}_{dom S} \in No \land S \in No \land {Z ↾}_{dom S} \in No) \to ((({a ↾}_{dom S}) <_{s} S \land \neg ({Z ↾}_{dom S}) <_{s} S) \to ({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}))$
167	162 159 164 166	syl3anc	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to ((({a ↾}_{dom S}) <_{s} S \land \neg ({Z ↾}_{dom S}) <_{s} S) \to ({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}))$
168	155 156 167	mp2and	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to ({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S})$
169		sltres	$⊢ (a \in No \land Z \in No \land dom S \in On) \to (({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}) \to a <_{s} Z)$
170	158 163 160 169	syl3anc	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to (({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}) \to a <_{s} Z)$
171	168 170	mpd	$⊢ (((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \land a \in A) \to a <_{s} Z$
172	171	ralrimiva	$⊢ ((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \to \forall a \in A a <_{s} Z$
173	150 172	impbida	$⊢ (A \subseteq No \land A \in V \land Z \in No) \to (\forall a \in A a <_{s} Z \leftrightarrow \neg ({Z ↾}_{dom S}) <_{s} S)$

Metamath Proof Explorer

Theorem nosupbnd2

Proof