MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  madebday Structured version   Visualization version   GIF version

Theorem madebday 27631
Description: A surreal is part of the set made by ordinal 𝐴 iff its birthday is less than or equal to 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
Assertion
Ref Expression
madebday ((𝐴 ∈ On ∧ 𝑋 No ) → (𝑋 ∈ ( M ‘𝐴) ↔ ( bday 𝑋) ⊆ 𝐴))

Proof of Theorem madebday
Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 madebdayim 27619 . 2 (𝑋 ∈ ( M ‘𝐴) → ( bday 𝑋) ⊆ 𝐴)
2 sseq2 4007 . . . . . . 7 (𝑎 = 𝑏 → (( bday 𝑥) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝑏))
3 fveq2 6890 . . . . . . . 8 (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏))
43eleq2d 2817 . . . . . . 7 (𝑎 = 𝑏 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝑏)))
52, 4imbi12d 343 . . . . . 6 (𝑎 = 𝑏 → ((( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ (( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏))))
65ralbidv 3175 . . . . 5 (𝑎 = 𝑏 → (∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 No (( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏))))
7 fveq2 6890 . . . . . . . 8 (𝑥 = 𝑦 → ( bday 𝑥) = ( bday 𝑦))
87sseq1d 4012 . . . . . . 7 (𝑥 = 𝑦 → (( bday 𝑥) ⊆ 𝑏 ↔ ( bday 𝑦) ⊆ 𝑏))
9 eleq1 2819 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘𝑏)))
108, 9imbi12d 343 . . . . . 6 (𝑥 = 𝑦 → ((( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏)) ↔ (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))))
1110cbvralvw 3232 . . . . 5 (∀𝑥 No (( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏)) ↔ ∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)))
126, 11bitrdi 286 . . . 4 (𝑎 = 𝑏 → (∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))))
13 sseq2 4007 . . . . . 6 (𝑎 = 𝐴 → (( bday 𝑥) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝐴))
14 fveq2 6890 . . . . . . 7 (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴))
1514eleq2d 2817 . . . . . 6 (𝑎 = 𝐴 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝐴)))
1613, 15imbi12d 343 . . . . 5 (𝑎 = 𝐴 → ((( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴))))
1716ralbidv 3175 . . . 4 (𝑎 = 𝐴 → (∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 No (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴))))
18 bdayelon 27514 . . . . . . . . 9 ( bday 𝑥) ∈ On
19 onsseleq 6404 . . . . . . . . 9 ((( bday 𝑥) ∈ On ∧ 𝑎 ∈ On) → (( bday 𝑥) ⊆ 𝑎 ↔ (( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎)))
2018, 19mpan 686 . . . . . . . 8 (𝑎 ∈ On → (( bday 𝑥) ⊆ 𝑎 ↔ (( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎)))
2120ad2antrr 722 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ⊆ 𝑎 ↔ (( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎)))
22 simpll 763 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → 𝑎 ∈ On)
23 onelss 6405 . . . . . . . . . . . . 13 (𝑎 ∈ On → (( bday 𝑥) ∈ 𝑎 → ( bday 𝑥) ⊆ 𝑎))
2423ad2antrr 722 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ∈ 𝑎 → ( bday 𝑥) ⊆ 𝑎))
2524imp 405 . . . . . . . . . . 11 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ( bday 𝑥) ⊆ 𝑎)
26 madess 27608 . . . . . . . . . . 11 ((𝑎 ∈ On ∧ ( bday 𝑥) ⊆ 𝑎) → ( M ‘( bday 𝑥)) ⊆ ( M ‘𝑎))
2722, 25, 26syl2an2r 681 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ( M ‘( bday 𝑥)) ⊆ ( M ‘𝑎))
28 ssid 4003 . . . . . . . . . . 11 ( bday 𝑥) ⊆ ( bday 𝑥)
29 simpr 483 . . . . . . . . . . . . 13 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ( bday 𝑥) ∈ 𝑎)
30 simplr 765 . . . . . . . . . . . . 13 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → 𝑥 No )
3129, 30jca 510 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → (( bday 𝑥) ∈ 𝑎𝑥 No ))
32 simpllr 772 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)))
33 sseq2 4007 . . . . . . . . . . . . . 14 (𝑏 = ( bday 𝑥) → (( bday 𝑦) ⊆ 𝑏 ↔ ( bday 𝑦) ⊆ ( bday 𝑥)))
34 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑏 = ( bday 𝑥) → ( M ‘𝑏) = ( M ‘( bday 𝑥)))
3534eleq2d 2817 . . . . . . . . . . . . . 14 (𝑏 = ( bday 𝑥) → (𝑦 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘( bday 𝑥))))
3633, 35imbi12d 343 . . . . . . . . . . . . 13 (𝑏 = ( bday 𝑥) → ((( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ↔ (( bday 𝑦) ⊆ ( bday 𝑥) → 𝑦 ∈ ( M ‘( bday 𝑥)))))
37 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ( bday 𝑦) = ( bday 𝑥))
3837sseq1d 4012 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (( bday 𝑦) ⊆ ( bday 𝑥) ↔ ( bday 𝑥) ⊆ ( bday 𝑥)))
39 eleq1 2819 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 ∈ ( M ‘( bday 𝑥)) ↔ 𝑥 ∈ ( M ‘( bday 𝑥))))
4038, 39imbi12d 343 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((( bday 𝑦) ⊆ ( bday 𝑥) → 𝑦 ∈ ( M ‘( bday 𝑥))) ↔ (( bday 𝑥) ⊆ ( bday 𝑥) → 𝑥 ∈ ( M ‘( bday 𝑥)))))
4136, 40rspc2v 3621 . . . . . . . . . . . 12 ((( bday 𝑥) ∈ 𝑎𝑥 No ) → (∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) → (( bday 𝑥) ⊆ ( bday 𝑥) → 𝑥 ∈ ( M ‘( bday 𝑥)))))
4231, 32, 41sylc 65 . . . . . . . . . . 11 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → (( bday 𝑥) ⊆ ( bday 𝑥) → 𝑥 ∈ ( M ‘( bday 𝑥))))
4328, 42mpi 20 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘( bday 𝑥)))
4427, 43sseldd 3982 . . . . . . . . 9 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘𝑎))
4544ex 411 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ∈ 𝑎𝑥 ∈ ( M ‘𝑎)))
46 madebdaylemlrcut 27630 . . . . . . . . . . . 12 ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥)
4718a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( bday 𝑥) ∈ On)
48 lltropt 27604 . . . . . . . . . . . . . . 15 ( L ‘𝑥) <<s ( R ‘𝑥)
4948a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( L ‘𝑥) <<s ( R ‘𝑥))
50 leftssold 27610 . . . . . . . . . . . . . . 15 ( L ‘𝑥) ⊆ ( O ‘( bday 𝑥))
5150a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( L ‘𝑥) ⊆ ( O ‘( bday 𝑥)))
52 rightssold 27611 . . . . . . . . . . . . . . 15 ( R ‘𝑥) ⊆ ( O ‘( bday 𝑥))
5352a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( R ‘𝑥) ⊆ ( O ‘( bday 𝑥)))
54 madecut 27614 . . . . . . . . . . . . . 14 (((( bday 𝑥) ∈ On ∧ ( L ‘𝑥) <<s ( R ‘𝑥)) ∧ (( L ‘𝑥) ⊆ ( O ‘( bday 𝑥)) ∧ ( R ‘𝑥) ⊆ ( O ‘( bday 𝑥)))) → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘( bday 𝑥)))
5547, 49, 51, 53, 54syl22anc 835 . . . . . . . . . . . . 13 (𝑥 No → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘( bday 𝑥)))
5655adantl 480 . . . . . . . . . . . 12 ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘( bday 𝑥)))
5746, 56eqeltrrd 2832 . . . . . . . . . . 11 ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘( bday 𝑥)))
58 raleq 3320 . . . . . . . . . . . . 13 (( bday 𝑥) = 𝑎 → (∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ↔ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))))
5958anbi1d 628 . . . . . . . . . . . 12 (( bday 𝑥) = 𝑎 → ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) ↔ (∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No )))
60 fveq2 6890 . . . . . . . . . . . . 13 (( bday 𝑥) = 𝑎 → ( M ‘( bday 𝑥)) = ( M ‘𝑎))
6160eleq2d 2817 . . . . . . . . . . . 12 (( bday 𝑥) = 𝑎 → (𝑥 ∈ ( M ‘( bday 𝑥)) ↔ 𝑥 ∈ ( M ‘𝑎)))
6259, 61imbi12d 343 . . . . . . . . . . 11 (( bday 𝑥) = 𝑎 → (((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘( bday 𝑥))) ↔ ((∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘𝑎))))
6357, 62mpbii 232 . . . . . . . . . 10 (( bday 𝑥) = 𝑎 → ((∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘𝑎)))
6463com12 32 . . . . . . . . 9 ((∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → (( bday 𝑥) = 𝑎𝑥 ∈ ( M ‘𝑎)))
6564adantll 710 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) = 𝑎𝑥 ∈ ( M ‘𝑎)))
6645, 65jaod 855 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → ((( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎) → 𝑥 ∈ ( M ‘𝑎)))
6721, 66sylbid 239 . . . . . 6 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)))
6867ralrimiva 3144 . . . . 5 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) → ∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)))
6968ex 411 . . . 4 (𝑎 ∈ On → (∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) → ∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎))))
7012, 17, 69tfis3 7849 . . 3 (𝐴 ∈ On → ∀𝑥 No (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴)))
71 fveq2 6890 . . . . . 6 (𝑥 = 𝑋 → ( bday 𝑥) = ( bday 𝑋))
7271sseq1d 4012 . . . . 5 (𝑥 = 𝑋 → (( bday 𝑥) ⊆ 𝐴 ↔ ( bday 𝑋) ⊆ 𝐴))
73 eleq1 2819 . . . . 5 (𝑥 = 𝑋 → (𝑥 ∈ ( M ‘𝐴) ↔ 𝑋 ∈ ( M ‘𝐴)))
7472, 73imbi12d 343 . . . 4 (𝑥 = 𝑋 → ((( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴)) ↔ (( bday 𝑋) ⊆ 𝐴𝑋 ∈ ( M ‘𝐴))))
7574rspccva 3610 . . 3 ((∀𝑥 No (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴)) ∧ 𝑋 No ) → (( bday 𝑋) ⊆ 𝐴𝑋 ∈ ( M ‘𝐴)))
7670, 75sylan 578 . 2 ((𝐴 ∈ On ∧ 𝑋 No ) → (( bday 𝑋) ⊆ 𝐴𝑋 ∈ ( M ‘𝐴)))
771, 76impbid2 225 1 ((𝐴 ∈ On ∧ 𝑋 No ) → (𝑋 ∈ ( M ‘𝐴) ↔ ( bday 𝑋) ⊆ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 843   = wceq 1539  wcel 2104  wral 3059  wss 3947   class class class wbr 5147  Oncon0 6363  cfv 6542  (class class class)co 7411   No csur 27379   bday cbday 27381   <<s csslt 27518   |s cscut 27520   M cmade 27574   O cold 27575   L cleft 27577   R cright 27578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  df-2o 8469  df-no 27382  df-slt 27383  df-bday 27384  df-sslt 27519  df-scut 27521  df-made 27579  df-old 27580  df-left 27582  df-right 27583
This theorem is referenced by:  oldbday  27632  newbday  27633  lrcut  27634  sltonold  27926
  Copyright terms: Public domain W3C validator