Metamath Proof Explorer

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 
|- ( 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 
|- ( ph -> X e. No )
negsproplem1.2 
|- ( ph -> Y e. No )
negsproplem1.3 
|- ( ph -> ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
Assertion negsproplem1 
|- ( ph -> ( ( -us ` X ) e. No /\ ( X  ( -us ` Y )

Proof

Step Hyp Ref Expression
1 negsproplem.1 
 |-  ( 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 )
2 negsproplem1.1 
 |-  ( ph -> X e. No )
3 negsproplem1.2 
 |-  ( ph -> Y e. No )
4 negsproplem1.3 
 |-  ( ph -> ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
5 2 3 jca 
 |-  ( ph -> ( X e. No /\ Y e. No ) )
6 fveq2 
 |-  ( x = X -> ( bday ` x ) = ( bday ` X ) )
7 6 uneq1d 
 |-  ( x = X -> ( ( bday ` x ) u. ( bday ` y ) ) = ( ( bday ` X ) u. ( bday ` y ) ) )
8 7 eleq1d 
 |-  ( x = X -> ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) <-> ( ( bday ` X ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) )
9 fveq2 
 |-  ( x = X -> ( -us ` x ) = ( -us ` X ) )
10 9 eleq1d 
 |-  ( x = X -> ( ( -us ` x ) e. No <-> ( -us ` X ) e. No ) )
11 breq1 
 |-  ( x = X -> ( x  X
12 9 breq2d 
 |-  ( x = X -> ( ( -us ` y )  ( -us ` y )
13 11 12 imbi12d 
 |-  ( x = X -> ( ( x  ( -us ` y )  ( X  ( -us ` y )
14 10 13 anbi12d 
 |-  ( x = X -> ( ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( -us ` X ) e. No /\ ( X  ( -us ` y )
15 8 14 imbi12d 
 |-  ( 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 )
16 fveq2 
 |-  ( y = Y -> ( bday ` y ) = ( bday ` Y ) )
17 16 uneq2d 
 |-  ( y = Y -> ( ( bday ` X ) u. ( bday ` y ) ) = ( ( bday ` X ) u. ( bday ` Y ) ) )
18 17 eleq1d 
 |-  ( y = Y -> ( ( ( bday ` X ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) <-> ( ( bday ` X ) u. ( bday ` Y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) )
19 breq2 
 |-  ( y = Y -> ( X  X
20 fveq2 
 |-  ( y = Y -> ( -us ` y ) = ( -us ` Y ) )
21 20 breq1d 
 |-  ( y = Y -> ( ( -us ` y )  ( -us ` Y )
22 19 21 imbi12d 
 |-  ( y = Y -> ( ( X  ( -us ` y )  ( X  ( -us ` Y )
23 22 anbi2d 
 |-  ( y = Y -> ( ( ( -us ` X ) e. No /\ ( X  ( -us ` y )  ( ( -us ` X ) e. No /\ ( X  ( -us ` Y )
24 18 23 imbi12d 
 |-  ( 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 )
25 15 24 rspc2v 
 |-  ( ( 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 )
26 5 1 4 25 syl3c 
 |-  ( ph -> ( ( -us ` X ) e. No /\ ( X  ( -us ` Y )