negsunif

Description: Uniformity property for surreal negation. If L and R are any cut that represents A , then they may be used instead of (LeftA ) and ( RightA ) in the definition of negation. (Contributed by Scott Fenton, 14-Feb-2025)

	Ref	Expression
Hypotheses	negsunif.1	$⊢ φ \to L ≪_{s} R$
	negsunif.2	$⊢ φ \to A = L \|_{s} R$
Assertion	negsunif	$⊢ φ \to +_{s} (A) = +_{s} [R] \|_{s} +_{s} [L]$

Proof

Step	Hyp	Ref	Expression
1		negsunif.1	$⊢ φ \to L ≪_{s} R$
2		negsunif.2	$⊢ φ \to A = L \|_{s} R$
3	1	scutcld	$⊢ φ \to L \|_{s} R \in No$
4	2 3	eqeltrd	$⊢ φ \to A \in No$
5		negsval	$⊢ A \in No \to +_{s} (A) = +_{s} [R (A)] \|_{s} +_{s} [L (A)]$
6	4 5	syl	$⊢ φ \to +_{s} (A) = +_{s} [R (A)] \|_{s} +_{s} [L (A)]$
7		negscut2	$⊢ A \in No \to +_{s} [R (A)] ≪_{s} +_{s} [L (A)]$
8	4 7	syl	$⊢ φ \to +_{s} [R (A)] ≪_{s} +_{s} [L (A)]$
9	1 2	cofcutr2d	$⊢ φ \to \forall c \in R (A) \exists d \in R d \leq_{s} c$
10		negsfn	$⊢ +_{s} Fn No$
11		ssltss2	$⊢ L ≪_{s} R \to R \subseteq No$
12	1 11	syl	$⊢ φ \to R \subseteq No$
13		breq2	$⊢ b = +_{s} (d) \to (+_{s} (c) \leq_{s} b \leftrightarrow +_{s} (c) \leq_{s} +_{s} (d))$
14	13	rexima	$⊢ (+_{s} Fn No \land R \subseteq No) \to (\exists b \in +_{s} [R] +_{s} (c) \leq_{s} b \leftrightarrow \exists d \in R +_{s} (c) \leq_{s} +_{s} (d))$
15	10 12 14	sylancr	$⊢ φ \to (\exists b \in +_{s} [R] +_{s} (c) \leq_{s} b \leftrightarrow \exists d \in R +_{s} (c) \leq_{s} +_{s} (d))$
16	15	ralbidv	$⊢ φ \to (\forall c \in R (A) \exists b \in +_{s} [R] +_{s} (c) \leq_{s} b \leftrightarrow \forall c \in R (A) \exists d \in R +_{s} (c) \leq_{s} +_{s} (d))$
17	12	adantr	$⊢ (φ \land c \in R (A)) \to R \subseteq No$
18	17	sselda	$⊢ ((φ \land c \in R (A)) \land d \in R) \to d \in No$
19		rightssno	$⊢ R (A) \subseteq No$
20	19	sseli	$⊢ c \in R (A) \to c \in No$
21	20	ad2antlr	$⊢ ((φ \land c \in R (A)) \land d \in R) \to c \in No$
22	18 21	slenegd	$⊢ ((φ \land c \in R (A)) \land d \in R) \to (d \leq_{s} c \leftrightarrow +_{s} (c) \leq_{s} +_{s} (d))$
23	22	rexbidva	$⊢ (φ \land c \in R (A)) \to (\exists d \in R d \leq_{s} c \leftrightarrow \exists d \in R +_{s} (c) \leq_{s} +_{s} (d))$
24	23	ralbidva	$⊢ φ \to (\forall c \in R (A) \exists d \in R d \leq_{s} c \leftrightarrow \forall c \in R (A) \exists d \in R +_{s} (c) \leq_{s} +_{s} (d))$
25	16 24	bitr4d	$⊢ φ \to (\forall c \in R (A) \exists b \in +_{s} [R] +_{s} (c) \leq_{s} b \leftrightarrow \forall c \in R (A) \exists d \in R d \leq_{s} c)$
26	9 25	mpbird	$⊢ φ \to \forall c \in R (A) \exists b \in +_{s} [R] +_{s} (c) \leq_{s} b$
27		breq1	$⊢ a = +_{s} (c) \to (a \leq_{s} b \leftrightarrow +_{s} (c) \leq_{s} b)$
28	27	rexbidv	$⊢ a = +_{s} (c) \to (\exists b \in +_{s} [R] a \leq_{s} b \leftrightarrow \exists b \in +_{s} [R] +_{s} (c) \leq_{s} b)$
29	28	ralima	$⊢ (+_{s} Fn No \land R (A) \subseteq No) \to (\forall a \in +_{s} [R (A)] \exists b \in +_{s} [R] a \leq_{s} b \leftrightarrow \forall c \in R (A) \exists b \in +_{s} [R] +_{s} (c) \leq_{s} b)$
30	10 19 29	mp2an	$⊢ \forall a \in +_{s} [R (A)] \exists b \in +_{s} [R] a \leq_{s} b \leftrightarrow \forall c \in R (A) \exists b \in +_{s} [R] +_{s} (c) \leq_{s} b$
31	26 30	sylibr	$⊢ φ \to \forall a \in +_{s} [R (A)] \exists b \in +_{s} [R] a \leq_{s} b$
32	1 2	cofcutr1d	$⊢ φ \to \forall c \in L (A) \exists d \in L c \leq_{s} d$
33		ssltss1	$⊢ L ≪_{s} R \to L \subseteq No$
34	1 33	syl	$⊢ φ \to L \subseteq No$
35		breq1	$⊢ b = +_{s} (d) \to (b \leq_{s} +_{s} (c) \leftrightarrow +_{s} (d) \leq_{s} +_{s} (c))$
36	35	rexima	$⊢ (+_{s} Fn No \land L \subseteq No) \to (\exists b \in +_{s} [L] b \leq_{s} +_{s} (c) \leftrightarrow \exists d \in L +_{s} (d) \leq_{s} +_{s} (c))$
37	10 34 36	sylancr	$⊢ φ \to (\exists b \in +_{s} [L] b \leq_{s} +_{s} (c) \leftrightarrow \exists d \in L +_{s} (d) \leq_{s} +_{s} (c))$
38	37	ralbidv	$⊢ φ \to (\forall c \in L (A) \exists b \in +_{s} [L] b \leq_{s} +_{s} (c) \leftrightarrow \forall c \in L (A) \exists d \in L +_{s} (d) \leq_{s} +_{s} (c))$
39		leftssno	$⊢ L (A) \subseteq No$
40	39	sseli	$⊢ c \in L (A) \to c \in No$
41	40	ad2antlr	$⊢ ((φ \land c \in L (A)) \land d \in L) \to c \in No$
42	34	adantr	$⊢ (φ \land c \in L (A)) \to L \subseteq No$
43	42	sselda	$⊢ ((φ \land c \in L (A)) \land d \in L) \to d \in No$
44	41 43	slenegd	$⊢ ((φ \land c \in L (A)) \land d \in L) \to (c \leq_{s} d \leftrightarrow +_{s} (d) \leq_{s} +_{s} (c))$
45	44	rexbidva	$⊢ (φ \land c \in L (A)) \to (\exists d \in L c \leq_{s} d \leftrightarrow \exists d \in L +_{s} (d) \leq_{s} +_{s} (c))$
46	45	ralbidva	$⊢ φ \to (\forall c \in L (A) \exists d \in L c \leq_{s} d \leftrightarrow \forall c \in L (A) \exists d \in L +_{s} (d) \leq_{s} +_{s} (c))$
47	38 46	bitr4d	$⊢ φ \to (\forall c \in L (A) \exists b \in +_{s} [L] b \leq_{s} +_{s} (c) \leftrightarrow \forall c \in L (A) \exists d \in L c \leq_{s} d)$
48	32 47	mpbird	$⊢ φ \to \forall c \in L (A) \exists b \in +_{s} [L] b \leq_{s} +_{s} (c)$
49		breq2	$⊢ a = +_{s} (c) \to (b \leq_{s} a \leftrightarrow b \leq_{s} +_{s} (c))$
50	49	rexbidv	$⊢ a = +_{s} (c) \to (\exists b \in +_{s} [L] b \leq_{s} a \leftrightarrow \exists b \in +_{s} [L] b \leq_{s} +_{s} (c))$
51	50	ralima	$⊢ (+_{s} Fn No \land L (A) \subseteq No) \to (\forall a \in +_{s} [L (A)] \exists b \in +_{s} [L] b \leq_{s} a \leftrightarrow \forall c \in L (A) \exists b \in +_{s} [L] b \leq_{s} +_{s} (c))$
52	10 39 51	mp2an	$⊢ \forall a \in +_{s} [L (A)] \exists b \in +_{s} [L] b \leq_{s} a \leftrightarrow \forall c \in L (A) \exists b \in +_{s} [L] b \leq_{s} +_{s} (c)$
53	48 52	sylibr	$⊢ φ \to \forall a \in +_{s} [L (A)] \exists b \in +_{s} [L] b \leq_{s} a$
54		fnfun	$⊢ +_{s} Fn No \to Fun +_{s}$
55	10 54	ax-mp	$⊢ Fun +_{s}$
56		ssltex2	$⊢ L ≪_{s} R \to R \in V$
57	1 56	syl	$⊢ φ \to R \in V$
58		funimaexg	$⊢ (Fun +_{s} \land R \in V) \to +_{s} [R] \in V$
59	55 57 58	sylancr	$⊢ φ \to +_{s} [R] \in V$
60		snex	$⊢ \{+_{s} (A)\} \in V$
61	60	a1i	$⊢ φ \to \{+_{s} (A)\} \in V$
62		imassrn	$⊢ +_{s} [R] \subseteq ran +_{s}$
63		negsfo	$⊢ +_{s} : No \underset{onto}{⟶} No$
64		forn	$⊢ +_{s} : No \underset{onto}{⟶} No \to ran +_{s} = No$
65	63 64	ax-mp	$⊢ ran +_{s} = No$
66	62 65	sseqtri	$⊢ +_{s} [R] \subseteq No$
67	66	a1i	$⊢ φ \to +_{s} [R] \subseteq No$
68	4	negscld	$⊢ φ \to +_{s} (A) \in No$
69	68	snssd	$⊢ φ \to \{+_{s} (A)\} \subseteq No$
70		velsn	$⊢ a \in \{+_{s} (A)\} \leftrightarrow a = +_{s} (A)$
71		fvelimab	$⊢ (+_{s} Fn No \land R \subseteq No) \to (b \in +_{s} [R] \leftrightarrow \exists d \in R +_{s} (d) = b)$
72	10 12 71	sylancr	$⊢ φ \to (b \in +_{s} [R] \leftrightarrow \exists d \in R +_{s} (d) = b)$
73	2	sneqd	$⊢ φ \to \{A\} = \{L \|_{s} R\}$
74	73	adantr	$⊢ (φ \land d \in R) \to \{A\} = \{L \|_{s} R\}$
75		scutcut	$⊢ L ≪_{s} R \to (L \|_{s} R \in No \land L ≪_{s} \{L \|_{s} R\} \land \{L \|_{s} R\} ≪_{s} R)$
76	1 75	syl	$⊢ φ \to (L \|_{s} R \in No \land L ≪_{s} \{L \|_{s} R\} \land \{L \|_{s} R\} ≪_{s} R)$
77	76	simp3d	$⊢ φ \to \{L \|_{s} R\} ≪_{s} R$
78	77	adantr	$⊢ (φ \land d \in R) \to \{L \|_{s} R\} ≪_{s} R$
79	74 78	eqbrtrd	$⊢ (φ \land d \in R) \to \{A\} ≪_{s} R$
80		snidg	$⊢ A \in No \to A \in \{A\}$
81	4 80	syl	$⊢ φ \to A \in \{A\}$
82	81	adantr	$⊢ (φ \land d \in R) \to A \in \{A\}$
83		simpr	$⊢ (φ \land d \in R) \to d \in R$
84	79 82 83	ssltsepcd	$⊢ (φ \land d \in R) \to A <_{s} d$
85	4	adantr	$⊢ (φ \land d \in R) \to A \in No$
86	12	sselda	$⊢ (φ \land d \in R) \to d \in No$
87	85 86	sltnegd	$⊢ (φ \land d \in R) \to (A <_{s} d \leftrightarrow +_{s} (d) <_{s} +_{s} (A))$
88	84 87	mpbid	$⊢ (φ \land d \in R) \to +_{s} (d) <_{s} +_{s} (A)$
89		breq1	$⊢ +_{s} (d) = b \to (+_{s} (d) <_{s} +_{s} (A) \leftrightarrow b <_{s} +_{s} (A))$
90	88 89	syl5ibcom	$⊢ (φ \land d \in R) \to (+_{s} (d) = b \to b <_{s} +_{s} (A))$
91	90	rexlimdva	$⊢ φ \to (\exists d \in R +_{s} (d) = b \to b <_{s} +_{s} (A))$
92	72 91	sylbid	$⊢ φ \to (b \in +_{s} [R] \to b <_{s} +_{s} (A))$
93		breq2	$⊢ a = +_{s} (A) \to (b <_{s} a \leftrightarrow b <_{s} +_{s} (A))$
94	93	imbi2d	$⊢ a = +_{s} (A) \to ((b \in +_{s} [R] \to b <_{s} a) \leftrightarrow (b \in +_{s} [R] \to b <_{s} +_{s} (A)))$
95	92 94	syl5ibrcom	$⊢ φ \to (a = +_{s} (A) \to (b \in +_{s} [R] \to b <_{s} a))$
96	70 95	biimtrid	$⊢ φ \to (a \in \{+_{s} (A)\} \to (b \in +_{s} [R] \to b <_{s} a))$
97	96	3imp	$⊢ (φ \land a \in \{+_{s} (A)\} \land b \in +_{s} [R]) \to b <_{s} a$
98	97	3com23	$⊢ (φ \land b \in +_{s} [R] \land a \in \{+_{s} (A)\}) \to b <_{s} a$
99	59 61 67 69 98	ssltd	$⊢ φ \to +_{s} [R] ≪_{s} \{+_{s} (A)\}$
100	6	sneqd	$⊢ φ \to \{+_{s} (A)\} = \{+_{s} [R (A)] \|_{s} +_{s} [L (A)]\}$
101	99 100	breqtrd	$⊢ φ \to +_{s} [R] ≪_{s} \{+_{s} [R (A)] \|_{s} +_{s} [L (A)]\}$
102		ssltex1	$⊢ L ≪_{s} R \to L \in V$
103	1 102	syl	$⊢ φ \to L \in V$
104		funimaexg	$⊢ (Fun +_{s} \land L \in V) \to +_{s} [L] \in V$
105	55 103 104	sylancr	$⊢ φ \to +_{s} [L] \in V$
106		imassrn	$⊢ +_{s} [L] \subseteq ran +_{s}$
107	106 65	sseqtri	$⊢ +_{s} [L] \subseteq No$
108	107	a1i	$⊢ φ \to +_{s} [L] \subseteq No$
109		fvelimab	$⊢ (+_{s} Fn No \land L \subseteq No) \to (b \in +_{s} [L] \leftrightarrow \exists c \in L +_{s} (c) = b)$
110	10 34 109	sylancr	$⊢ φ \to (b \in +_{s} [L] \leftrightarrow \exists c \in L +_{s} (c) = b)$
111	1	adantr	$⊢ (φ \land c \in L) \to L ≪_{s} R$
112	111 75	syl	$⊢ (φ \land c \in L) \to (L \|_{s} R \in No \land L ≪_{s} \{L \|_{s} R\} \land \{L \|_{s} R\} ≪_{s} R)$
113	112	simp2d	$⊢ (φ \land c \in L) \to L ≪_{s} \{L \|_{s} R\}$
114	73	adantr	$⊢ (φ \land c \in L) \to \{A\} = \{L \|_{s} R\}$
115	113 114	breqtrrd	$⊢ (φ \land c \in L) \to L ≪_{s} \{A\}$
116		simpr	$⊢ (φ \land c \in L) \to c \in L$
117	81	adantr	$⊢ (φ \land c \in L) \to A \in \{A\}$
118	115 116 117	ssltsepcd	$⊢ (φ \land c \in L) \to c <_{s} A$
119	34	sselda	$⊢ (φ \land c \in L) \to c \in No$
120	4	adantr	$⊢ (φ \land c \in L) \to A \in No$
121	119 120	sltnegd	$⊢ (φ \land c \in L) \to (c <_{s} A \leftrightarrow +_{s} (A) <_{s} +_{s} (c))$
122	118 121	mpbid	$⊢ (φ \land c \in L) \to +_{s} (A) <_{s} +_{s} (c)$
123		breq2	$⊢ +_{s} (c) = b \to (+_{s} (A) <_{s} +_{s} (c) \leftrightarrow +_{s} (A) <_{s} b)$
124	122 123	syl5ibcom	$⊢ (φ \land c \in L) \to (+_{s} (c) = b \to +_{s} (A) <_{s} b)$
125	124	rexlimdva	$⊢ φ \to (\exists c \in L +_{s} (c) = b \to +_{s} (A) <_{s} b)$
126	110 125	sylbid	$⊢ φ \to (b \in +_{s} [L] \to +_{s} (A) <_{s} b)$
127		breq1	$⊢ a = +_{s} (A) \to (a <_{s} b \leftrightarrow +_{s} (A) <_{s} b)$
128	127	imbi2d	$⊢ a = +_{s} (A) \to ((b \in +_{s} [L] \to a <_{s} b) \leftrightarrow (b \in +_{s} [L] \to +_{s} (A) <_{s} b))$
129	126 128	syl5ibrcom	$⊢ φ \to (a = +_{s} (A) \to (b \in +_{s} [L] \to a <_{s} b))$
130	70 129	biimtrid	$⊢ φ \to (a \in \{+_{s} (A)\} \to (b \in +_{s} [L] \to a <_{s} b))$
131	130	3imp	$⊢ (φ \land a \in \{+_{s} (A)\} \land b \in +_{s} [L]) \to a <_{s} b$
132	61 105 69 108 131	ssltd	$⊢ φ \to \{+_{s} (A)\} ≪_{s} +_{s} [L]$
133	100 132	eqbrtrrd	$⊢ φ \to \{+_{s} [R (A)] \|_{s} +_{s} [L (A)]\} ≪_{s} +_{s} [L]$
134	8 31 53 101 133	cofcut1d	$⊢ φ \to +_{s} [R (A)] \|_{s} +_{s} [L (A)] = +_{s} [R] \|_{s} +_{s} [L]$
135	6 134	eqtrd	$⊢ φ \to +_{s} (A) = +_{s} [R] \|_{s} +_{s} [L]$

Metamath Proof Explorer

Theorem negsunif

Proof