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 No B No bday A = bday B A < s B x No bday x bday A A < s x x < s B

Proof

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