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	35	suceqd	$⊢ (ι 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$
37	36	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}$
38		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$
39	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_{𝑜}⟩$
40	39	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_{𝑜}⟩\}$
41	38 40	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_{𝑜}⟩\}$
42	37 41	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_{𝑜}⟩\}))$
43	42	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_{𝑜}⟩\}))$
44	34 43	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_{𝑜}⟩\}))$
45	32 44	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_{𝑜}⟩\})$
46		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_{𝑜}⟩\}$
47	1 46	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_{𝑜}⟩\}$
48	23 47	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_{𝑜}⟩\}$
49	48	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_{𝑜}⟩\})$
50		2on	$⊢ 2_{𝑜} \in On$
51	50	elexi	$⊢ 2_{𝑜} \in V$
52	51	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)\}$
53	52	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)\}$
54		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_{𝑜}⟩\}$
55		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)\}$
56	53 54 55	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)$
57	49 56	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)$
58	57	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)}$
59	58	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)}$
60	48	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_{𝑜}⟩\}$
61	59 60	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_{𝑜}⟩\}))$
62	45 61	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$
63	62	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))$
64	21 63	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)$
65	64	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$
66	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
67	66	3adant3	$⊢ (A \subseteq No \land A \in V \land Z \in No) \to S \in No$
68	67	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$
69		nodmon	$⊢ S \in No \to dom S \in On$
70	68 69	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$
71		noreson	$⊢ (S \in No \land dom S \in On) \to {S ↾}_{dom S} \in No$
72	68 70 71	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$
73		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$
74		noreson	$⊢ (Z \in No \land dom S \in On) \to {Z ↾}_{dom S} \in No$
75	73 70 74	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$
76		dmres	$⊢ dom ({S ↾}_{dom S}) = dom S \cap dom S$
77		inss2	$⊢ dom S \cap dom S \subseteq dom S$
78	76 77	eqsstri	$⊢ dom ({S ↾}_{dom S}) \subseteq dom S$
79	78	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$
80		dmres	$⊢ dom ({Z ↾}_{dom S}) = dom S \cap dom Z$
81		inss1	$⊢ dom S \cap dom Z \subseteq dom S$
82	80 81	eqsstri	$⊢ dom ({Z ↾}_{dom S}) \subseteq dom S$
83	82	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$
84	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}))\}$
85	84	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})))$
86	85	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})))$
87		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$
88		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$
89		breq1	$⊢ a = p \to (a <_{s} Z \leftrightarrow p <_{s} Z)$
90	89	rspcv	$⊢ p \in A \to (\forall a \in A a <_{s} Z \to p <_{s} Z)$
91	87 88 90	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$
92		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$
93	92	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$
94	93 87	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$
95	73	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$
96		ltsso	$⊢ <_{s} Or No$
97		soasym	$⊢ (<_{s} Or No \land (p \in No \land Z \in No)) \to (p <_{s} Z \to \neg Z <_{s} p)$
98	96 97	mpan	$⊢ (p \in No \land Z \in No) \to (p <_{s} Z \to \neg Z <_{s} p)$
99	94 95 98	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)$
100	91 99	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$
101		nodmon	$⊢ p \in No \to dom p \in On$
102	94 101	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$
103		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$
104		onelon	$⊢ (dom p \in On \land g \in dom p) \to g \in On$
105	102 103 104	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$
106		onsucb	$⊢ g \in On \leftrightarrow suc g \in On$
107	105 106	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$
108		ltsres	$⊢ (Z \in No \land p \in No \land suc g \in On) \to (({Z ↾}_{suc g}) <_{s} ({p ↾}_{suc g}) \to Z <_{s} p)$
109	95 94 107 108	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)$
110	100 109	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})$
111		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$
112		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$
113	92 112	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)$
114	113	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)$
115		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})$
116		breq1	$⊢ v = q \to (v <_{s} p \leftrightarrow q <_{s} p)$
117	116	notbid	$⊢ v = q \to (\neg v <_{s} p \leftrightarrow \neg q <_{s} p)$
118		reseq1	$⊢ v = q \to {v ↾}_{suc g} = {q ↾}_{suc g}$
119	118	eqeq2d	$⊢ v = q \to ({p ↾}_{suc g} = {v ↾}_{suc g} \leftrightarrow {p ↾}_{suc g} = {q ↾}_{suc g})$
120	117 119	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}))$
121	120	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})$
122	115 121	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})$
123	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}$
124	111 114 87 103 122 123	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}$
125	124	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}))$
126	110 125	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})$
127	126	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}))$
128	86 127	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}))$
129	128	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})$
130	68	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$
131		nodmord	$⊢ S \in No \to Ord dom S$
132	130 131	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$
133		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$
134		ordsucss	$⊢ Ord dom S \to (g \in dom S \to suc g \subseteq dom S)$
135	132 133 134	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$
136	135	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}$
137	135	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}$
138	136 137	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}))$
139	129 138	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})$
140	139	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})$
141		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})$
142	72 75 79 83 140 141	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})$
143		nofun	$⊢ S \in No \to Fun S$
144		funrel	$⊢ Fun S \to Rel S$
145		resdm	$⊢ Rel S \to {S ↾}_{dom S} = S$
146	68 143 144 145	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$
147	146	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)$
148	142 147	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$
149	65 148	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$
150		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$
151		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$
152		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$
153	1	nosupbnd1	$⊢ (A \subseteq No \land A \in V \land a \in A) \to ({a ↾}_{dom S}) <_{s} S$
154	150 151 152 153	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$
155		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$
156		simpl1	$⊢ ((A \subseteq No \land A \in V \land Z \in No) \land \neg ({Z ↾}_{dom S}) <_{s} S) \to A \subseteq No$
157	156	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$
158	150 151 66	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$
159	158 69	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$
160		noreson	$⊢ (a \in No \land dom S \in On) \to {a ↾}_{dom S} \in No$
161	157 159 160	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$
162		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$
163	162 159 74	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$
164		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}))$
165	96 164	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}))$
166	161 158 163 165	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}))$
167	154 155 166	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})$
168		ltsres	$⊢ (a \in No \land Z \in No \land dom S \in On) \to (({a ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}) \to a <_{s} Z)$
169	157 162 159 168	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)$
170	167 169	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$
171	170	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$
172	149 171	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