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<sB→∃x∈Nobday⁡x∈bday⁡A∧A<sx∧x<sB

Proof

Step Hyp Ref Expression
1 nodenselem6 ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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<sB→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<sB→⋂a∈On|A⁡a≠B⁡a∈bday⁡A
6 bdayfo ⊢bday:No⟶ontoOn
7 fof ⊢bday:No⟶ontoOn→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<sB→⋂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<sB→bday⁡A=dom⁡A
15 12 14 sseqtrd ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→⋂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<sB→⋂a∈On|A⁡a≠B⁡a∩dom⁡A=⋂a∈On|A⁡a≠B⁡a
18 4 17 eqtrid ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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<sB→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<sB→bday⁡A↾⋂a∈On|A⁡a≠B⁡a∈bday⁡A
21 nodenselem4 ⊢A∈No∧B∈No∧A<sB→⋂a∈On|A⁡a≠B⁡a∈On
22 21 adantrl ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→⋂a∈On|A⁡a≠B⁡a∈On
23 nodenselem8 ⊢A∈No∧B∈No∧bday⁡A=bday⁡B→A<sB↔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<sB→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<sB→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<sB→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<sB→A⁡⋂a∈On|A⁡a≠B⁡a=1𝑜
28 eqid ⊢∅=∅
29 27 28 jctir ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A⁡⋂a∈On|A⁡a≠B⁡a=1𝑜∧∅=∅
30 29 3mix1d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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⁡a1𝑜∅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<sB→A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅1𝑜2𝑜∅2𝑜∅
35 19 fveq2d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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<sB→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<sB→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<sB→A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅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⁡aA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y
43 39 42 jctil ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→∀y∈⋂a∈On|A⁡a≠B⁡aA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅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∈xA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y↔∀y∈⋂a∈On|A⁡a≠B⁡aA⁡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⁡x1𝑜∅1𝑜2𝑜∅2𝑜A↾⋂a∈On|A⁡a≠B⁡a⁡x↔A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅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∈xA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜A↾⋂a∈On|A⁡a≠B⁡a⁡x↔∀y∈⋂a∈On|A⁡a≠B⁡aA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅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⁡aA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅1𝑜2𝑜∅2𝑜A↾⋂a∈On|A⁡a≠B⁡a⁡⋂a∈On|A⁡a≠B⁡a→∃x∈On∀y∈xA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡x1𝑜∅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<sB→∃x∈On∀y∈xA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜A↾⋂a∈On|A⁡a≠B⁡a⁡x
51 simpll ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A∈No
52 sltval ⊢A∈No∧A↾⋂a∈On|A⁡a≠B⁡a∈No→A<sA↾⋂a∈On|A⁡a≠B⁡a↔∃x∈On∀y∈xA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡x1𝑜∅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<sB→A<sA↾⋂a∈On|A⁡a≠B⁡a↔∃x∈On∀y∈xA⁡y=A↾⋂a∈On|A⁡a≠B⁡a⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜A↾⋂a∈On|A⁡a≠B⁡a⁡x
54 50 53 mpbird ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A<sA↾⋂a∈On|A⁡a≠B⁡a
55 41 adantl ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB∧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<sB→y∈⋂a∈On|A⁡a≠B⁡a→A⁡y=B⁡y
57 56 imp ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB∧y∈⋂a∈On|A⁡a≠B⁡a→A⁡y=B⁡y
58 55 57 eqtr3d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB∧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<sB→∀y∈⋂a∈On|A⁡a≠B⁡aA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y
60 26 simprd ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→B⁡⋂a∈On|A⁡a≠B⁡a=2𝑜
61 60 28 jctil ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→∅=∅∧B⁡⋂a∈On|A⁡a≠B⁡a=2𝑜
62 61 3mix3d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→∅=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<sB→∅1𝑜∅1𝑜2𝑜∅2𝑜B⁡⋂a∈On|A⁡a≠B⁡a
66 38 65 eqbrtrd ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A↾⋂a∈On|A⁡a≠B⁡a⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅1𝑜2𝑜∅2𝑜B⁡⋂a∈On|A⁡a≠B⁡a
67 raleq ⊢x=⋂a∈On|A⁡a≠B⁡a→∀y∈xA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y↔∀y∈⋂a∈On|A⁡a≠B⁡aA↾⋂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⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x↔A↾⋂a∈On|A⁡a≠B⁡a⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅1𝑜2𝑜∅2𝑜B⁡⋂a∈On|A⁡a≠B⁡a
70 67 69 anbi12d ⊢x=⋂a∈On|A⁡a≠B⁡a→∀y∈xA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x↔∀y∈⋂a∈On|A⁡a≠B⁡aA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅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⁡aA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅1𝑜2𝑜∅2𝑜B⁡⋂a∈On|A⁡a≠B⁡a→∃x∈On∀y∈xA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
72 22 59 66 71 syl12anc ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→∃x∈On∀y∈xA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
73 simplr ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→B∈No
74 sltval ⊢A↾⋂a∈On|A⁡a≠B⁡a∈No∧B∈No→A↾⋂a∈On|A⁡a≠B⁡a<sB↔∃x∈On∀y∈xA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
75 1 73 74 syl2anc ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A↾⋂a∈On|A⁡a≠B⁡a<sB↔∃x∈On∀y∈xA↾⋂a∈On|A⁡a≠B⁡a⁡y=B⁡y∧A↾⋂a∈On|A⁡a≠B⁡a⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
76 72 75 mpbird ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A↾⋂a∈On|A⁡a≠B⁡a<sB
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<sx↔A<sA↾⋂a∈On|A⁡a≠B⁡a
80 breq1 ⊢x=A↾⋂a∈On|A⁡a≠B⁡a→x<sB↔A↾⋂a∈On|A⁡a≠B⁡a<sB
81 78 79 80 3anbi123d ⊢x=A↾⋂a∈On|A⁡a≠B⁡a→bday⁡x∈bday⁡A∧A<sx∧x<sB↔bday⁡A↾⋂a∈On|A⁡a≠B⁡a∈bday⁡A∧A<sA↾⋂a∈On|A⁡a≠B⁡a∧A↾⋂a∈On|A⁡a≠B⁡a<sB
82 81 rspcev ⊢A↾⋂a∈On|A⁡a≠B⁡a∈No∧bday⁡A↾⋂a∈On|A⁡a≠B⁡a∈bday⁡A∧A<sA↾⋂a∈On|A⁡a≠B⁡a∧A↾⋂a∈On|A⁡a≠B⁡a<sB→∃x∈Nobday⁡x∈bday⁡A∧A<sx∧x<sB
83 1 20 54 76 82 syl13anc ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→∃x∈Nobday⁡x∈bday⁡A∧A<sx∧x<sB