noinfdm

Description: Next, we calculate the domain of T . This is mostly to change bound variables. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Hypothesis	noinfdm.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	Assertion	noinfdm	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to dom T = \{z \| \exists p \in B (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$

Proof

Step	Hyp	Ref	Expression
1		noinfdm.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		iffalse	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))) = (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
3	1 2	syl5eq	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to T = (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
4	3	dmeqd	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to dom T = dom (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
5		iotaex	$⊢ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)) \in V$
6		eqid	$⊢ (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) = (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
7	5 6	dmmpti	$⊢ dom (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) = \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\}$
8		eleq1w	$⊢ y = z \to (y \in dom u \leftrightarrow z \in dom u)$
9		suceq	$⊢ y = z \to suc y = suc z$
10	9	reseq2d	$⊢ y = z \to {u ↾}_{suc y} = {u ↾}_{suc z}$
11	9	reseq2d	$⊢ y = z \to {v ↾}_{suc y} = {v ↾}_{suc z}$
12	10 11	eqeq12d	$⊢ y = z \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc z} = {v ↾}_{suc z})$
13	12	imbi2d	$⊢ y = z \to ((\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z}))$
14	13	ralbidv	$⊢ y = z \to (\forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z}))$
15	8 14	anbi12d	$⊢ y = z \to ((y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (z \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z})))$
16	15	rexbidv	$⊢ y = z \to (\exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists u \in B (z \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z})))$
17		dmeq	$⊢ u = p \to dom u = dom p$
18	17	eleq2d	$⊢ u = p \to (z \in dom u \leftrightarrow z \in dom p)$
19		breq1	$⊢ u = p \to (u <_{s} v \leftrightarrow p <_{s} v)$
20	19	notbid	$⊢ u = p \to (\neg u <_{s} v \leftrightarrow \neg p <_{s} v)$
21		reseq1	$⊢ u = p \to {u ↾}_{suc z} = {p ↾}_{suc z}$
22	21	eqeq1d	$⊢ u = p \to ({u ↾}_{suc z} = {v ↾}_{suc z} \leftrightarrow {p ↾}_{suc z} = {v ↾}_{suc z})$
23	20 22	imbi12d	$⊢ u = p \to ((\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z}) \leftrightarrow (\neg p <_{s} v \to {p ↾}_{suc z} = {v ↾}_{suc z}))$
24	23	ralbidv	$⊢ u = p \to (\forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z}) \leftrightarrow \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc z} = {v ↾}_{suc z}))$
25		breq2	$⊢ v = q \to (p <_{s} v \leftrightarrow p <_{s} q)$
26	25	notbid	$⊢ v = q \to (\neg p <_{s} v \leftrightarrow \neg p <_{s} q)$
27		reseq1	$⊢ v = q \to {v ↾}_{suc z} = {q ↾}_{suc z}$
28	27	eqeq2d	$⊢ v = q \to ({p ↾}_{suc z} = {v ↾}_{suc z} \leftrightarrow {p ↾}_{suc z} = {q ↾}_{suc z})$
29	26 28	imbi12d	$⊢ v = q \to ((\neg p <_{s} v \to {p ↾}_{suc z} = {v ↾}_{suc z}) \leftrightarrow (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))$
30	29	cbvralvw	$⊢ \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc z} = {v ↾}_{suc z}) \leftrightarrow \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z})$
31	24 30	bitrdi	$⊢ u = p \to (\forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z}) \leftrightarrow \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))$
32	18 31	anbi12d	$⊢ u = p \to ((z \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z})) \leftrightarrow (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z})))$
33	32	cbvrexvw	$⊢ \exists u \in B (z \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc z} = {v ↾}_{suc z})) \leftrightarrow \exists p \in B (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))$
34	16 33	bitrdi	$⊢ y = z \to (\exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists p \in B (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z})))$
35	34	cbvabv	$⊢ \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} = \{z \| \exists p \in B (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$
36	7 35	eqtri	$⊢ dom (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) = \{z \| \exists p \in B (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$
37	4 36	eqtrdi	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to dom T = \{z \| \exists p \in B (z \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$

Metamath Proof Explorer

Theorem noinfdm

Proof