Metamath Proof Explorer

Theorem nodense

Description: Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Axiom SD of Alling p. 184. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion nodense 
|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  E. x e. No ( ( bday ` x ) e. ( bday ` A ) /\ A

Proof

Step Hyp Ref Expression
1 nodenselem6 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No )
2 bdayval 
 |-  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No -> ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) = dom ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
3 1 2 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) = dom ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
4 dmres 
 |-  dom ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } i^i dom A )
5 nodenselem5 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) )
6 bdayfo 
 |-  bday : No -onto-> On
7 fof 
 |-  ( bday : No -onto-> On -> bday : No --> On )
8 6 7 ax-mp 
 |-  bday : No --> On
9 0elon 
 |-  (/) e. On
10 8 9 f0cli 
 |-  ( bday ` A ) e. On
11 10 onelssi 
 |-  ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } C_ ( bday ` A ) )
12 5 11 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } C_ ( bday ` A ) )
13 bdayval 
 |-  ( A e. No -> ( bday ` A ) = dom A )
14 13 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` A ) = dom A )
15 12 14 sseqtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } C_ dom A )
16 df-ss 
 |-  ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } C_ dom A <-> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } i^i dom A ) = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
17 15 16 sylib 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } i^i dom A ) = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
18 4 17 eqtrid 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  dom ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
19 3 18 eqtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
20 19 5 eqeltrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) e. ( bday ` A ) )
21 nodenselem4 
 |-  ( ( ( A e. No /\ B e. No ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
22 21 adantrl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
23 nodenselem8 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
24 23 biimpd 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
25 24 3expia 
 |-  ( ( A e. No /\ B e. No ) -> ( ( bday ` A ) = ( bday ` B ) -> ( A  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) ) )
26 25 imp32 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) )
27 26 simpld 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o )
28 eqid 
 |-  (/) = (/)
29 27 28 jctir 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ (/) = (/) ) )
30 29 3mix1d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ (/) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ (/) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ (/) = 2o ) ) )
31 fvex 
 |-  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
32 0ex 
 |-  (/) e. _V
33 31 32 brtp 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) <-> ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ (/) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ (/) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ (/) = 2o ) ) )
34 30 33 sylibr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) )
35 19 fveq2d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
36 fvnobday 
 |-  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No -> ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) = (/) )
37 1 36 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) = (/) )
38 35 37 eqtr3d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
39 34 38 breqtrrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
40 fvres 
 |-  ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( A ` y ) )
41 40 eqcomd 
 |-  ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) )
42 41 rgen 
 |-  A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y )
43 39 42 jctil 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
44 raleq 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A. y e. x ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) <-> A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) ) )
45 fveq2 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` x ) = ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
46 fveq2 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
47 45 46 breq12d 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) <-> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
48 44 47 anbi12d 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A. y e. x ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) ) <-> ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) )
49 48 rspcev 
 |-  ( ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) -> E. x e. On ( A. y e. x ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) ) )
50 22 43 49 syl2anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  E. x e. On ( A. y e. x ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) ) )
51 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  A e. No )
52 sltval 
 |-  ( ( A e. No /\ ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) ) ) )
53 51 1 52 syl2anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A  E. x e. On ( A. y e. x ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) ) ) )
54 50 53 mpbird 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  A
55 41 adantl 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A ` y ) = ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) )
56 nodenselem7 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` y ) = ( B ` y ) ) )
57 56 imp 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A ` y ) = ( B ` y ) )
58 55 57 eqtr3d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) )
59 58 ralrimiva 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) )
60 26 simprd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o )
61 60 28 jctil 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( (/) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) )
62 61 3mix3d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( (/) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( (/) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( (/) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
63 fvex 
 |-  ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
64 32 63 brtp 
 |-  ( (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) <-> ( ( (/) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( (/) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( (/) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
65 62 64 sylibr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
66 38 65 eqbrtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
67 raleq 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A. y e. x ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) <-> A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) ) )
68 fveq2 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( B ` x ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
69 46 68 breq12d 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
70 67 69 anbi12d 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A. y e. x ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) )
71 70 rspcev 
 |-  ( ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) -> E. x e. On ( A. y e. x ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
72 22 59 66 71 syl12anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  E. x e. On ( A. y e. x ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
73 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  B e. No )
74 sltval 
 |-  ( ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No /\ B e. No ) -> ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )  E. x e. On ( A. y e. x ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
75 1 73 74 syl2anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )  E. x e. On ( A. y e. x ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` y ) = ( B ` y ) /\ ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
76 72 75 mpbird 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
77 fveq2 
 |-  ( x = ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( bday ` x ) = ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
78 77 eleq1d 
 |-  ( x = ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( ( bday ` x ) e. ( bday ` A ) <-> ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) e. ( bday ` A ) ) )
79 breq2 
 |-  ( x = ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( A  A
80 breq1 
 |-  ( x = ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( x  ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
81 78 79 80 3anbi123d 
 |-  ( x = ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( ( ( bday ` x ) e. ( bday ` A ) /\ A  ( ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) e. ( bday ` A ) /\ A
82 81 rspcev 
 |-  ( ( ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No /\ ( ( bday ` ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) e. ( bday ` A ) /\ A  E. x e. No ( ( bday ` x ) e. ( bday ` A ) /\ A
83 1 20 54 76 82 syl13anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  E. x e. No ( ( bday ` x ) e. ( bday ` A ) /\ A