nosupcbv

Description: Lemma to change bound variables in a surreal supremum. (Contributed by Scott Fenton, 9-Aug-2024)

		Ref	Expression
	Hypothesis	nosupcbv.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	nosupcbv	$⊢ S = if (\exists a \in A \forall b \in A \neg a <_{s} b, (ι a \in A \| \forall b \in A \neg a <_{s} b) \cup \{⟨dom (ι a \in A \| \forall b \in A \neg a <_{s} b), 2_{𝑜}⟩\}, (c \in \{d \| \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))))$

Proof

Step	Hyp	Ref	Expression
1		nosupcbv.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		breq1	$⊢ x = a \to (x <_{s} y \leftrightarrow a <_{s} y)$
3	2	notbid	$⊢ x = a \to (\neg x <_{s} y \leftrightarrow \neg a <_{s} y)$
4	3	ralbidv	$⊢ x = a \to (\forall y \in A \neg x <_{s} y \leftrightarrow \forall y \in A \neg a <_{s} y)$
5		breq2	$⊢ y = b \to (a <_{s} y \leftrightarrow a <_{s} b)$
6	5	notbid	$⊢ y = b \to (\neg a <_{s} y \leftrightarrow \neg a <_{s} b)$
7	6	cbvralvw	$⊢ \forall y \in A \neg a <_{s} y \leftrightarrow \forall b \in A \neg a <_{s} b$
8	4 7	bitrdi	$⊢ x = a \to (\forall y \in A \neg x <_{s} y \leftrightarrow \forall b \in A \neg a <_{s} b)$
9	8	cbvrexvw	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \leftrightarrow \exists a \in A \forall b \in A \neg a <_{s} b$
10	8	cbvriotavw	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) = (ι a \in A \| \forall b \in A \neg a <_{s} b)$
11	10	dmeqi	$⊢ dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = dom (ι a \in A \| \forall b \in A \neg a <_{s} b)$
12	11	opeq1i	$⊢ ⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩ = ⟨dom (ι a \in A \| \forall b \in A \neg a <_{s} b), 2_{𝑜}⟩$
13	12	sneqi	$⊢ \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\} = \{⟨dom (ι a \in A \| \forall b \in A \neg a <_{s} b), 2_{𝑜}⟩\}$
14	10 13	uneq12i	$⊢ (ι 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_{𝑜}⟩\} = (ι a \in A \| \forall b \in A \neg a <_{s} b) \cup \{⟨dom (ι a \in A \| \forall b \in A \neg a <_{s} b), 2_{𝑜}⟩\}$
15		eleq1w	$⊢ g = c \to (g \in dom u \leftrightarrow c \in dom u)$
16		suceq	$⊢ g = c \to suc g = suc c$
17	16	reseq2d	$⊢ g = c \to {u ↾}_{suc g} = {u ↾}_{suc c}$
18	16	reseq2d	$⊢ g = c \to {v ↾}_{suc g} = {v ↾}_{suc c}$
19	17 18	eqeq12d	$⊢ g = c \to ({u ↾}_{suc g} = {v ↾}_{suc g} \leftrightarrow {u ↾}_{suc c} = {v ↾}_{suc c})$
20	19	imbi2d	$⊢ g = c \to ((\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}))$
21	20	ralbidv	$⊢ g = c \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}))$
22		fveqeq2	$⊢ g = c \to (u (g) = x \leftrightarrow u (c) = x)$
23	15 21 22	3anbi123d	$⊢ g = c \to ((g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x) \leftrightarrow (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x))$
24	23	rexbidv	$⊢ g = c \to (\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) \leftrightarrow \exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x))$
25	24	iotabidv	$⊢ g = c \to (ι 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 \| \exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x))$
26		eqeq2	$⊢ x = a \to (u (c) = x \leftrightarrow u (c) = a)$
27	26	3anbi3d	$⊢ x = a \to ((c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x) \leftrightarrow (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = a))$
28	27	rexbidv	$⊢ x = a \to (\exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x) \leftrightarrow \exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = a))$
29		dmeq	$⊢ u = e \to dom u = dom e$
30	29	eleq2d	$⊢ u = e \to (c \in dom u \leftrightarrow c \in dom e)$
31		breq2	$⊢ u = e \to (v <_{s} u \leftrightarrow v <_{s} e)$
32	31	notbid	$⊢ u = e \to (\neg v <_{s} u \leftrightarrow \neg v <_{s} e)$
33		reseq1	$⊢ u = e \to {u ↾}_{suc c} = {e ↾}_{suc c}$
34	33	eqeq1d	$⊢ u = e \to ({u ↾}_{suc c} = {v ↾}_{suc c} \leftrightarrow {e ↾}_{suc c} = {v ↾}_{suc c})$
35	32 34	imbi12d	$⊢ u = e \to ((\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \leftrightarrow (\neg v <_{s} e \to {e ↾}_{suc c} = {v ↾}_{suc c}))$
36	35	ralbidv	$⊢ u = e \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \leftrightarrow \forall v \in A (\neg v <_{s} e \to {e ↾}_{suc c} = {v ↾}_{suc c}))$
37		breq1	$⊢ v = f \to (v <_{s} e \leftrightarrow f <_{s} e)$
38	37	notbid	$⊢ v = f \to (\neg v <_{s} e \leftrightarrow \neg f <_{s} e)$
39		reseq1	$⊢ v = f \to {v ↾}_{suc c} = {f ↾}_{suc c}$
40	39	eqeq2d	$⊢ v = f \to ({e ↾}_{suc c} = {v ↾}_{suc c} \leftrightarrow {e ↾}_{suc c} = {f ↾}_{suc c})$
41	38 40	imbi12d	$⊢ v = f \to ((\neg v <_{s} e \to {e ↾}_{suc c} = {v ↾}_{suc c}) \leftrightarrow (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}))$
42	41	cbvralvw	$⊢ \forall v \in A (\neg v <_{s} e \to {e ↾}_{suc c} = {v ↾}_{suc c}) \leftrightarrow \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c})$
43	36 42	bitrdi	$⊢ u = e \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \leftrightarrow \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}))$
44		fveq1	$⊢ u = e \to u (c) = e (c)$
45	44	eqeq1d	$⊢ u = e \to (u (c) = a \leftrightarrow e (c) = a)$
46	30 43 45	3anbi123d	$⊢ u = e \to ((c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = a) \leftrightarrow (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))$
47	46	cbvrexvw	$⊢ \exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = a) \leftrightarrow \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a)$
48	28 47	bitrdi	$⊢ x = a \to (\exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x) \leftrightarrow \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))$
49	48	cbviotavw	$⊢ (ι x \| \exists u \in A (c \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc c} = {v ↾}_{suc c}) \land u (c) = x)) = (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))$
50	25 49	eqtrdi	$⊢ g = c \to (ι 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)) = (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))$
51	50	cbvmptv	$⊢ (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))) = (c \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}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a)))$
52		eleq1w	$⊢ y = d \to (y \in dom u \leftrightarrow d \in dom u)$
53		suceq	$⊢ y = d \to suc y = suc d$
54	53	reseq2d	$⊢ y = d \to {u ↾}_{suc y} = {u ↾}_{suc d}$
55	53	reseq2d	$⊢ y = d \to {v ↾}_{suc y} = {v ↾}_{suc d}$
56	54 55	eqeq12d	$⊢ y = d \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc d} = {v ↾}_{suc d})$
57	56	imbi2d	$⊢ y = d \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d}))$
58	57	ralbidv	$⊢ y = d \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d}))$
59	52 58	anbi12d	$⊢ y = d \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (d \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d})))$
60	59	rexbidv	$⊢ y = d \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 u \in A (d \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d})))$
61	29	eleq2d	$⊢ u = e \to (d \in dom u \leftrightarrow d \in dom e)$
62		reseq1	$⊢ u = e \to {u ↾}_{suc d} = {e ↾}_{suc d}$
63	62	eqeq1d	$⊢ u = e \to ({u ↾}_{suc d} = {v ↾}_{suc d} \leftrightarrow {e ↾}_{suc d} = {v ↾}_{suc d})$
64	32 63	imbi12d	$⊢ u = e \to ((\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d}) \leftrightarrow (\neg v <_{s} e \to {e ↾}_{suc d} = {v ↾}_{suc d}))$
65	64	ralbidv	$⊢ u = e \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d}) \leftrightarrow \forall v \in A (\neg v <_{s} e \to {e ↾}_{suc d} = {v ↾}_{suc d}))$
66		reseq1	$⊢ v = f \to {v ↾}_{suc d} = {f ↾}_{suc d}$
67	66	eqeq2d	$⊢ v = f \to ({e ↾}_{suc d} = {v ↾}_{suc d} \leftrightarrow {e ↾}_{suc d} = {f ↾}_{suc d})$
68	38 67	imbi12d	$⊢ v = f \to ((\neg v <_{s} e \to {e ↾}_{suc d} = {v ↾}_{suc d}) \leftrightarrow (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))$
69	68	cbvralvw	$⊢ \forall v \in A (\neg v <_{s} e \to {e ↾}_{suc d} = {v ↾}_{suc d}) \leftrightarrow \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d})$
70	65 69	bitrdi	$⊢ u = e \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d}) \leftrightarrow \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))$
71	61 70	anbi12d	$⊢ u = e \to ((d \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d})) \leftrightarrow (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d})))$
72	71	cbvrexvw	$⊢ \exists u \in A (d \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc d} = {v ↾}_{suc d})) \leftrightarrow \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))$
73	60 72	bitrdi	$⊢ y = d \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 e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d})))$
74	73	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}))\} = \{d \| \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))\}$
75	74	mpteq1i	$⊢ (c \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}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))) = (c \in \{d \| \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a)))$
76	51 75	eqtri	$⊢ (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))) = (c \in \{d \| \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a)))$
77	9 14 76	ifbieq12i	$⊢ 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)))) = if (\exists a \in A \forall b \in A \neg a <_{s} b, (ι a \in A \| \forall b \in A \neg a <_{s} b) \cup \{⟨dom (ι a \in A \| \forall b \in A \neg a <_{s} b), 2_{𝑜}⟩\}, (c \in \{d \| \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))))$
78	1 77	eqtri	$⊢ S = if (\exists a \in A \forall b \in A \neg a <_{s} b, (ι a \in A \| \forall b \in A \neg a <_{s} b) \cup \{⟨dom (ι a \in A \| \forall b \in A \neg a <_{s} b), 2_{𝑜}⟩\}, (c \in \{d \| \exists e \in A (d \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc d} = {f ↾}_{suc d}))\} ⟼ (ι a \| \exists e \in A (c \in dom e \land \forall f \in A (\neg f <_{s} e \to {e ↾}_{suc c} = {f ↾}_{suc c}) \land e (c) = a))))$

Metamath Proof Explorer

Theorem nosupcbv

Proof