nosupdm

Description: The domain of the surreal supremum when there is no maximum. The primary point of this theorem is to change bound variable. (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Hypothesis	nosupdm.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	nosupdm	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$

Proof

Step	Hyp	Ref	Expression
1		nosupdm.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		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)))$
3	1 2	syl5eq	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to S = (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)))$
4	3	dmeqd	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = 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)))$
5		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$
6		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)))$
7	5 6	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}))\}$
8	4 7	eqtrdi	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{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}))\}$
9		dmeq	$⊢ u = p \to dom u = dom p$
10	9	eleq2d	$⊢ u = p \to (y \in dom u \leftrightarrow y \in dom p)$
11		breq1	$⊢ v = q \to (v <_{s} u \leftrightarrow q <_{s} u)$
12	11	notbid	$⊢ v = q \to (\neg v <_{s} u \leftrightarrow \neg q <_{s} u)$
13		reseq1	$⊢ v = q \to {v ↾}_{suc y} = {q ↾}_{suc y}$
14	13	eqeq2d	$⊢ v = q \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc y} = {q ↾}_{suc y})$
15	12 14	imbi12d	$⊢ v = q \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg q <_{s} u \to {u ↾}_{suc y} = {q ↾}_{suc y}))$
16	15	cbvralvw	$⊢ \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall q \in A (\neg q <_{s} u \to {u ↾}_{suc y} = {q ↾}_{suc y})$
17		breq2	$⊢ u = p \to (q <_{s} u \leftrightarrow q <_{s} p)$
18	17	notbid	$⊢ u = p \to (\neg q <_{s} u \leftrightarrow \neg q <_{s} p)$
19		reseq1	$⊢ u = p \to {u ↾}_{suc y} = {p ↾}_{suc y}$
20	19	eqeq1d	$⊢ u = p \to ({u ↾}_{suc y} = {q ↾}_{suc y} \leftrightarrow {p ↾}_{suc y} = {q ↾}_{suc y})$
21	18 20	imbi12d	$⊢ u = p \to ((\neg q <_{s} u \to {u ↾}_{suc y} = {q ↾}_{suc y}) \leftrightarrow (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y}))$
22	21	ralbidv	$⊢ u = p \to (\forall q \in A (\neg q <_{s} u \to {u ↾}_{suc y} = {q ↾}_{suc y}) \leftrightarrow \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y}))$
23	16 22	syl5bb	$⊢ u = p \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y}))$
24	10 23	anbi12d	$⊢ u = p \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (y \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y})))$
25	24	cbvrexvw	$⊢ \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 p \in A (y \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y}))$
26		eleq1w	$⊢ y = z \to (y \in dom p \leftrightarrow z \in dom p)$
27		suceq	$⊢ y = z \to suc y = suc z$
28	27	reseq2d	$⊢ y = z \to {p ↾}_{suc y} = {p ↾}_{suc z}$
29	27	reseq2d	$⊢ y = z \to {q ↾}_{suc y} = {q ↾}_{suc z}$
30	28 29	eqeq12d	$⊢ y = z \to ({p ↾}_{suc y} = {q ↾}_{suc y} \leftrightarrow {p ↾}_{suc z} = {q ↾}_{suc z})$
31	30	imbi2d	$⊢ y = z \to ((\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y}) \leftrightarrow (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))$
32	31	ralbidv	$⊢ y = z \to (\forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y}) \leftrightarrow \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))$
33	26 32	anbi12d	$⊢ y = z \to ((y \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y})) \leftrightarrow (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z})))$
34	33	rexbidv	$⊢ y = z \to (\exists p \in A (y \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc y} = {q ↾}_{suc y})) \leftrightarrow \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z})))$
35	25 34	syl5bb	$⊢ y = z \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 p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z})))$
36	35	cbvabv	$⊢ \{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 \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$
37	8 36	eqtrdi	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$

Metamath Proof Explorer

Theorem nosupdm

Proof