Metamath Proof Explorer

Theorem negsprop

Description: Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsprop 
|- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )

Proof

Step Hyp Ref Expression
1 bdayelon 
 |-  ( bday ` A ) e. On
2 bdayelon 
 |-  ( bday ` B ) e. On
3 1 2 onun2i 
 |-  ( ( bday ` A ) u. ( bday ` B ) ) e. On
4 risset 
 |-  ( ( ( bday ` A ) u. ( bday ` B ) ) e. On <-> E. a e. On a = ( ( bday ` A ) u. ( bday ` B ) ) )
5 3 4 mpbi 
 |-  E. a e. On a = ( ( bday ` A ) u. ( bday ` B ) )
6 eqeq1 
 |-  ( a = b -> ( a = ( ( bday ` p ) u. ( bday ` q ) ) <-> b = ( ( bday ` p ) u. ( bday ` q ) ) ) )
7 6 imbi1d 
 |-  ( a = b -> ( ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
8 7 2ralbidv 
 |-  ( a = b -> ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  A. p e. No A. q e. No ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
9 fveq2 
 |-  ( p = x -> ( bday ` p ) = ( bday ` x ) )
10 9 uneq1d 
 |-  ( p = x -> ( ( bday ` p ) u. ( bday ` q ) ) = ( ( bday ` x ) u. ( bday ` q ) ) )
11 10 eqeq2d 
 |-  ( p = x -> ( b = ( ( bday ` p ) u. ( bday ` q ) ) <-> b = ( ( bday ` x ) u. ( bday ` q ) ) ) )
12 fveq2 
 |-  ( p = x -> ( -us ` p ) = ( -us ` x ) )
13 12 eleq1d 
 |-  ( p = x -> ( ( -us ` p ) e. No <-> ( -us ` x ) e. No ) )
14 breq1 
 |-  ( p = x -> ( p  x
15 12 breq2d 
 |-  ( p = x -> ( ( -us ` q )  ( -us ` q )
16 14 15 imbi12d 
 |-  ( p = x -> ( ( p  ( -us ` q )  ( x  ( -us ` q )
17 13 16 anbi12d 
 |-  ( p = x -> ( ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  ( ( -us ` x ) e. No /\ ( x  ( -us ` q )
18 11 17 imbi12d 
 |-  ( p = x -> ( ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  ( b = ( ( bday ` x ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` q )
19 fveq2 
 |-  ( q = y -> ( bday ` q ) = ( bday ` y ) )
20 19 uneq2d 
 |-  ( q = y -> ( ( bday ` x ) u. ( bday ` q ) ) = ( ( bday ` x ) u. ( bday ` y ) ) )
21 20 eqeq2d 
 |-  ( q = y -> ( b = ( ( bday ` x ) u. ( bday ` q ) ) <-> b = ( ( bday ` x ) u. ( bday ` y ) ) ) )
22 breq2 
 |-  ( q = y -> ( x  x
23 fveq2 
 |-  ( q = y -> ( -us ` q ) = ( -us ` y ) )
24 23 breq1d 
 |-  ( q = y -> ( ( -us ` q )  ( -us ` y )
25 22 24 imbi12d 
 |-  ( q = y -> ( ( x  ( -us ` q )  ( x  ( -us ` y )
26 25 anbi2d 
 |-  ( q = y -> ( ( ( -us ` x ) e. No /\ ( x  ( -us ` q )  ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
27 21 26 imbi12d 
 |-  ( q = y -> ( ( b = ( ( bday ` x ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` q )  ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
28 18 27 cbvral2vw 
 |-  ( A. p e. No A. q e. No ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
29 8 28 bitrdi 
 |-  ( a = b -> ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
30 raleq 
 |-  ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
31 ralrot3 
 |-  ( A. x e. No A. y e. No A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
32 r19.23v 
 |-  ( A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
33 risset 
 |-  ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) <-> E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) )
34 33 imbi1i 
 |-  ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
35 32 34 bitr4i 
 |-  ( A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
36 35 2ralbii 
 |-  ( A. x e. No A. y e. No A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
37 31 36 bitr3i 
 |-  ( A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
38 30 37 bitrdi 
 |-  ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
39 simpr 
 |-  ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
40 simpll 
 |-  ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  p e. No )
41 39 40 negsproplem3 
 |-  ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( -us ` p ) e. No /\ ( -us " ( _Right ` p ) ) <
42 41 simp1d 
 |-  ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( -us ` p ) e. No )
43 simplr 
 |-  ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
44 simplll 
 |-  ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  p e. No )
45 simpllr 
 |-  ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  q e. No )
46 simpr 
 |-  ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  p
47 43 44 45 46 negsproplem7 
 |-  ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( -us ` q )
48 47 ex 
 |-  ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( p  ( -us ` q )
49 42 48 jca 
 |-  ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
50 49 expcom 
 |-  ( A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( p e. No /\ q e. No ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
51 38 50 syl6bi 
 |-  ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( p e. No /\ q e. No ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
52 51 com3l 
 |-  ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( p e. No /\ q e. No ) -> ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
53 52 ralrimivv 
 |-  ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
54 53 a1i 
 |-  ( a e. On -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
55 29 54 tfis2 
 |-  ( a e. On -> A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )
56 fveq2 
 |-  ( p = A -> ( bday ` p ) = ( bday ` A ) )
57 56 uneq1d 
 |-  ( p = A -> ( ( bday ` p ) u. ( bday ` q ) ) = ( ( bday ` A ) u. ( bday ` q ) ) )
58 57 eqeq2d 
 |-  ( p = A -> ( a = ( ( bday ` p ) u. ( bday ` q ) ) <-> a = ( ( bday ` A ) u. ( bday ` q ) ) ) )
59 fveq2 
 |-  ( p = A -> ( -us ` p ) = ( -us ` A ) )
60 59 eleq1d 
 |-  ( p = A -> ( ( -us ` p ) e. No <-> ( -us ` A ) e. No ) )
61 breq1 
 |-  ( p = A -> ( p  A
62 59 breq2d 
 |-  ( p = A -> ( ( -us ` q )  ( -us ` q )
63 61 62 imbi12d 
 |-  ( p = A -> ( ( p  ( -us ` q )  ( A  ( -us ` q )
64 60 63 anbi12d 
 |-  ( p = A -> ( ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  ( ( -us ` A ) e. No /\ ( A  ( -us ` q )
65 58 64 imbi12d 
 |-  ( p = A -> ( ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  ( a = ( ( bday ` A ) u. ( bday ` q ) ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` q )
66 fveq2 
 |-  ( q = B -> ( bday ` q ) = ( bday ` B ) )
67 66 uneq2d 
 |-  ( q = B -> ( ( bday ` A ) u. ( bday ` q ) ) = ( ( bday ` A ) u. ( bday ` B ) ) )
68 67 eqeq2d 
 |-  ( q = B -> ( a = ( ( bday ` A ) u. ( bday ` q ) ) <-> a = ( ( bday ` A ) u. ( bday ` B ) ) ) )
69 breq2 
 |-  ( q = B -> ( A  A
70 fveq2 
 |-  ( q = B -> ( -us ` q ) = ( -us ` B ) )
71 70 breq1d 
 |-  ( q = B -> ( ( -us ` q )  ( -us ` B )
72 69 71 imbi12d 
 |-  ( q = B -> ( ( A  ( -us ` q )  ( A  ( -us ` B )
73 72 anbi2d 
 |-  ( q = B -> ( ( ( -us ` A ) e. No /\ ( A  ( -us ` q )  ( ( -us ` A ) e. No /\ ( A  ( -us ` B )
74 68 73 imbi12d 
 |-  ( q = B -> ( ( a = ( ( bday ` A ) u. ( bday ` q ) ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` q )  ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )
75 65 74 rspc2v 
 |-  ( ( A e. No /\ B e. No ) -> ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p  ( -us ` q )  ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )
76 55 75 syl5com 
 |-  ( a e. On -> ( ( A e. No /\ B e. No ) -> ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )
77 76 com23 
 |-  ( a e. On -> ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )
78 77 rexlimiv 
 |-  ( E. a e. On a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )
79 5 78 ax-mp 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` B )