Theorem negsproplem1

Description: Lemma for surreal negation. We prove a pair of properties of surreal negation simultaneously. First, we instantiate some quantifiers. (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
	negsproplem1.1	$$⊢\phi \to X\in \mathrm{No}$$
	negsproplem1.2	$$⊢\phi \to Y\in \mathrm{No}$$
	negsproplem1.3	$$⊢\phi \to \mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(Y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
Assertion	negsproplem1	$$⊢\phi \to \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}Y\to {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
2		negsproplem1.1	$$⊢\phi \to X\in \mathrm{No}$$
3		negsproplem1.2	$$⊢\phi \to Y\in \mathrm{No}$$
4		negsproplem1.3	$$⊢\phi \to \mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(Y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
5	2 3	jca	$$⊢\phi \to \left(X\in \mathrm{No}\wedge Y\in \mathrm{No}\right)$$
6		fveq2	$$⊢x=X\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(X\right)$$
7	6	uneq1d	$$⊢x=X\to \mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)=\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(y\right)$$
8	7	eleq1d	$$⊢x=X\to \left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\leftrightarrow \mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\right)$$
9		fveq2	$$⊢x=X\to {+}_s\left(x\right)={+}_s\left(X\right)$$
10	9	eleq1d	$$⊢x=X\to \left({+}_s\left(x\right)\in \mathrm{No}\leftrightarrow {+}_s\left(X\right)\in \mathrm{No}\right)$$
11		breq1	$$⊢x=X\to \left(x{<}_{s}y\leftrightarrow X{<}_{s}y\right)$$
12	9	breq2d	$$⊢x=X\to \left({+}_s\left(y\right){<}_s{+}_s\left(x\right)\leftrightarrow {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)$$
13	11 12	imbi12d	$$⊢x=X\to \left(\left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\leftrightarrow \left(X{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)\right)$$
14	10 13	anbi12d	$$⊢x=X\to \left(\left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\leftrightarrow \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)\right)\right)$$
15	8 14	imbi12d	$$⊢x=X\to \left(\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)\leftrightarrow \left(\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)\right)\right)\right)$$
16		fveq2	$$⊢y=Y\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(Y\right)$$
17	16	uneq2d	$$⊢y=Y\to \mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(y\right)=\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(Y\right)$$
18	17	eleq1d	$$⊢y=Y\to \left(\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\leftrightarrow \mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(Y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\right)$$
19		breq2	$$⊢y=Y\to \left(X{<}_{s}y\leftrightarrow X{<}_{s}Y\right)$$
20		fveq2	$$⊢y=Y\to {+}_s\left(y\right)={+}_s\left(Y\right)$$
21	20	breq1d	$$⊢y=Y\to \left({+}_s\left(y\right){<}_s{+}_s\left(X\right)\leftrightarrow {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)$$
22	19 21	imbi12d	$$⊢y=Y\to \left(\left(X{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)\leftrightarrow \left(X{<}_{s}Y\to {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)\right)$$
23	22	anbi2d	$$⊢y=Y\to \left(\left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)\right)\leftrightarrow \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}Y\to {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)\right)\right)$$
24	18 23	imbi12d	$$⊢y=Y\to \left(\left(\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(X\right)\right)\right)\right)\leftrightarrow \left(\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(Y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}Y\to {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)\right)\right)\right)$$
25	15 24	rspc2v	$$⊢\left(X\in \mathrm{No}\wedge Y\in \mathrm{No}\right)\to \left(\forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)\to \left(\mathrm{bday}\left(X\right)\cup \mathrm{bday}\left(Y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}Y\to {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)\right)\right)\right)$$
26	5 1 4 25	syl3c	$$⊢\phi \to \left({+}_s\left(X\right)\in \mathrm{No}\wedge \left(X{<}_{s}Y\to {+}_s\left(Y\right){<}_s{+}_s\left(X\right)\right)\right)$$