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	No typesetting found for |- ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
	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	Could not format assertion : No typesetting found for |- ( ph -> ( ( -us ` X ) e. No /\ ( X ( -us ` Y )

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	Could not format ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
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	Could not format ( x = X -> ( -us ` x ) = ( -us ` X ) ) : No typesetting found for |- ( x = X -> ( -us ` x ) = ( -us ` X ) ) with typecode |-
10	9	eleq1d	Could not format ( x = X -> ( ( -us ` x ) e. No <-> ( -us ` X ) e. No ) ) : No typesetting found for |- ( x = X -> ( ( -us ` x ) e. No <-> ( -us ` X ) e. No ) ) with typecode |-
11		breq1	$$⊢x=X\to \left(x{<}_{s}y\leftrightarrow X{<}_{s}y\right)$$
12	9	breq2d	Could not format ( x = X -> ( ( -us ` y ) ( -us ` y ) ( ( -us ` y ) ( -us ` y )
13	11 12	imbi12d	Could not format ( x = X -> ( ( x ( -us ` y ) ( X ( -us ` y ) ( ( x ( -us ` y ) ( X ( -us ` y )
14	10 13	anbi12d	Could not format ( x = X -> ( ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` X ) e. No /\ ( X ( -us ` y ) ( ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` X ) e. No /\ ( X ( -us ` y )
15	8 14	imbi12d	Could not format ( x = X -> ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` X ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` y ) ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` X ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` y )
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	Could not format ( y = Y -> ( -us ` y ) = ( -us ` Y ) ) : No typesetting found for |- ( y = Y -> ( -us ` y ) = ( -us ` Y ) ) with typecode |-
21	20	breq1d	Could not format ( y = Y -> ( ( -us ` y ) ( -us ` Y ) ( ( -us ` y ) ( -us ` Y )
22	19 21	imbi12d	Could not format ( y = Y -> ( ( X ( -us ` y ) ( X ( -us ` Y ) ( ( X ( -us ` y ) ( X ( -us ` Y )
23	22	anbi2d	Could not format ( y = Y -> ( ( ( -us ` X ) e. No /\ ( X ( -us ` y ) ( ( -us ` X ) e. No /\ ( X ( -us ` Y ) ( ( ( -us ` X ) e. No /\ ( X ( -us ` y ) ( ( -us ` X ) e. No /\ ( X ( -us ` Y )
24	18 23	imbi12d	Could not format ( y = Y -> ( ( ( ( bday ` X ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` y ) ( ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` Y ) ( ( ( ( bday ` X ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` y ) ( ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` Y )
25	15 24	rspc2v	Could not format ( ( X e. No /\ Y e. No ) -> ( A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` Y ) ( A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` X ) e. No /\ ( X ( -us ` Y )
26	5 1 4 25	syl3c	Could not format ( ph -> ( ( -us ` X ) e. No /\ ( X ( -us ` Y ) ( ( -us ` X ) e. No /\ ( X ( -us ` Y )