noinfcbv

Description: Change bound variables for surreal infimum. (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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

Metamath Proof Explorer

Theorem noinfcbv

Proof