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

Theorem madebday 27394
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 27382 . 2 (𝑋 ∈ ( M ‘𝐴) → ( bday 𝑋) ⊆ 𝐴)
2 sseq2 4009 . . . . . . 7 (𝑎 = 𝑏 → (( bday 𝑥) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝑏))
3 fveq2 6892 . . . . . . . 8 (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏))
43eleq2d 2820 . . . . . . 7 (𝑎 = 𝑏 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝑏)))
52, 4imbi12d 345 . . . . . 6 (𝑎 = 𝑏 → ((( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ (( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏))))
65ralbidv 3178 . . . . 5 (𝑎 = 𝑏 → (∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 No (( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏))))
7 fveq2 6892 . . . . . . . 8 (𝑥 = 𝑦 → ( bday 𝑥) = ( bday 𝑦))
87sseq1d 4014 . . . . . . 7 (𝑥 = 𝑦 → (( bday 𝑥) ⊆ 𝑏 ↔ ( bday 𝑦) ⊆ 𝑏))
9 eleq1 2822 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘𝑏)))
108, 9imbi12d 345 . . . . . 6 (𝑥 = 𝑦 → ((( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏)) ↔ (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))))
1110cbvralvw 3235 . . . . 5 (∀𝑥 No (( bday 𝑥) ⊆ 𝑏𝑥 ∈ ( M ‘𝑏)) ↔ ∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)))
126, 11bitrdi 287 . . . 4 (𝑎 = 𝑏 → (∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))))
13 sseq2 4009 . . . . . 6 (𝑎 = 𝐴 → (( bday 𝑥) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝐴))
14 fveq2 6892 . . . . . . 7 (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴))
1514eleq2d 2820 . . . . . 6 (𝑎 = 𝐴 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝐴)))
1613, 15imbi12d 345 . . . . 5 (𝑎 = 𝐴 → ((( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴))))
1716ralbidv 3178 . . . 4 (𝑎 = 𝐴 → (∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 No (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴))))
18 bdayelon 27278 . . . . . . . . 9 ( bday 𝑥) ∈ On
19 onsseleq 6406 . . . . . . . . 9 ((( bday 𝑥) ∈ On ∧ 𝑎 ∈ On) → (( bday 𝑥) ⊆ 𝑎 ↔ (( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎)))
2018, 19mpan 689 . . . . . . . 8 (𝑎 ∈ On → (( bday 𝑥) ⊆ 𝑎 ↔ (( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎)))
2120ad2antrr 725 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ⊆ 𝑎 ↔ (( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎)))
22 simpll 766 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → 𝑎 ∈ On)
23 onelss 6407 . . . . . . . . . . . . 13 (𝑎 ∈ On → (( bday 𝑥) ∈ 𝑎 → ( bday 𝑥) ⊆ 𝑎))
2423ad2antrr 725 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ∈ 𝑎 → ( bday 𝑥) ⊆ 𝑎))
2524imp 408 . . . . . . . . . . 11 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ( bday 𝑥) ⊆ 𝑎)
26 madess 27371 . . . . . . . . . . 11 ((𝑎 ∈ On ∧ ( bday 𝑥) ⊆ 𝑎) → ( M ‘( bday 𝑥)) ⊆ ( M ‘𝑎))
2722, 25, 26syl2an2r 684 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ( M ‘( bday 𝑥)) ⊆ ( M ‘𝑎))
28 ssid 4005 . . . . . . . . . . 11 ( bday 𝑥) ⊆ ( bday 𝑥)
29 simpr 486 . . . . . . . . . . . . 13 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ( bday 𝑥) ∈ 𝑎)
30 simplr 768 . . . . . . . . . . . . 13 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → 𝑥 No )
3129, 30jca 513 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → (( bday 𝑥) ∈ 𝑎𝑥 No ))
32 simpllr 775 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)))
33 sseq2 4009 . . . . . . . . . . . . . 14 (𝑏 = ( bday 𝑥) → (( bday 𝑦) ⊆ 𝑏 ↔ ( bday 𝑦) ⊆ ( bday 𝑥)))
34 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑏 = ( bday 𝑥) → ( M ‘𝑏) = ( M ‘( bday 𝑥)))
3534eleq2d 2820 . . . . . . . . . . . . . 14 (𝑏 = ( bday 𝑥) → (𝑦 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘( bday 𝑥))))
3633, 35imbi12d 345 . . . . . . . . . . . . 13 (𝑏 = ( bday 𝑥) → ((( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ↔ (( bday 𝑦) ⊆ ( bday 𝑥) → 𝑦 ∈ ( M ‘( bday 𝑥)))))
37 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ( bday 𝑦) = ( bday 𝑥))
3837sseq1d 4014 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (( bday 𝑦) ⊆ ( bday 𝑥) ↔ ( bday 𝑥) ⊆ ( bday 𝑥)))
39 eleq1 2822 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 ∈ ( M ‘( bday 𝑥)) ↔ 𝑥 ∈ ( M ‘( bday 𝑥))))
4038, 39imbi12d 345 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((( bday 𝑦) ⊆ ( bday 𝑥) → 𝑦 ∈ ( M ‘( bday 𝑥))) ↔ (( bday 𝑥) ⊆ ( bday 𝑥) → 𝑥 ∈ ( M ‘( bday 𝑥)))))
4136, 40rspc2v 3623 . . . . . . . . . . . 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 3984 . . . . . . . . 9 ((((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) ∧ ( bday 𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘𝑎))
4544ex 414 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ∈ 𝑎𝑥 ∈ ( M ‘𝑎)))
46 madebdaylemlrcut 27393 . . . . . . . . . . . 12 ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥)
4718a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( bday 𝑥) ∈ On)
48 lltropt 27367 . . . . . . . . . . . . . . 15 ( L ‘𝑥) <<s ( R ‘𝑥)
4948a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( L ‘𝑥) <<s ( R ‘𝑥))
50 leftssold 27373 . . . . . . . . . . . . . . 15 ( L ‘𝑥) ⊆ ( O ‘( bday 𝑥))
5150a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( L ‘𝑥) ⊆ ( O ‘( bday 𝑥)))
52 rightssold 27374 . . . . . . . . . . . . . . 15 ( R ‘𝑥) ⊆ ( O ‘( bday 𝑥))
5352a1i 11 . . . . . . . . . . . . . 14 (𝑥 No → ( R ‘𝑥) ⊆ ( O ‘( bday 𝑥)))
54 madecut 27377 . . . . . . . . . . . . . 14 (((( bday 𝑥) ∈ On ∧ ( L ‘𝑥) <<s ( R ‘𝑥)) ∧ (( L ‘𝑥) ⊆ ( O ‘( bday 𝑥)) ∧ ( R ‘𝑥) ⊆ ( O ‘( bday 𝑥)))) → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘( bday 𝑥)))
5547, 49, 51, 53, 54syl22anc 838 . . . . . . . . . . . . 13 (𝑥 No → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘( bday 𝑥)))
5655adantl 483 . . . . . . . . . . . 12 ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘( bday 𝑥)))
5746, 56eqeltrrd 2835 . . . . . . . . . . 11 ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘( bday 𝑥)))
58 raleq 3323 . . . . . . . . . . . . 13 (( bday 𝑥) = 𝑎 → (∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ↔ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))))
5958anbi1d 631 . . . . . . . . . . . 12 (( bday 𝑥) = 𝑎 → ((∀𝑏 ∈ ( bday 𝑥)∀𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No ) ↔ (∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 No )))
60 fveq2 6892 . . . . . . . . . . . . 13 (( bday 𝑥) = 𝑎 → ( M ‘( bday 𝑥)) = ( M ‘𝑎))
6160eleq2d 2820 . . . . . . . . . . . 12 (( bday 𝑥) = 𝑎 → (𝑥 ∈ ( M ‘( bday 𝑥)) ↔ 𝑥 ∈ ( M ‘𝑎)))
6259, 61imbi12d 345 . . . . . . . . . . 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 713 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) = 𝑎𝑥 ∈ ( M ‘𝑎)))
6645, 65jaod 858 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → ((( bday 𝑥) ∈ 𝑎 ∨ ( bday 𝑥) = 𝑎) → 𝑥 ∈ ( M ‘𝑎)))
6721, 66sylbid 239 . . . . . 6 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 No ) → (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)))
6867ralrimiva 3147 . . . . 5 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏))) → ∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎)))
6968ex 414 . . . 4 (𝑎 ∈ On → (∀𝑏𝑎𝑦 No (( bday 𝑦) ⊆ 𝑏𝑦 ∈ ( M ‘𝑏)) → ∀𝑥 No (( bday 𝑥) ⊆ 𝑎𝑥 ∈ ( M ‘𝑎))))
7012, 17, 69tfis3 7847 . . 3 (𝐴 ∈ On → ∀𝑥 No (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴)))
71 fveq2 6892 . . . . . 6 (𝑥 = 𝑋 → ( bday 𝑥) = ( bday 𝑋))
7271sseq1d 4014 . . . . 5 (𝑥 = 𝑋 → (( bday 𝑥) ⊆ 𝐴 ↔ ( bday 𝑋) ⊆ 𝐴))
73 eleq1 2822 . . . . 5 (𝑥 = 𝑋 → (𝑥 ∈ ( M ‘𝐴) ↔ 𝑋 ∈ ( M ‘𝐴)))
7472, 73imbi12d 345 . . . 4 (𝑥 = 𝑋 → ((( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴)) ↔ (( bday 𝑋) ⊆ 𝐴𝑋 ∈ ( M ‘𝐴))))
7574rspccva 3612 . . 3 ((∀𝑥 No (( bday 𝑥) ⊆ 𝐴𝑥 ∈ ( M ‘𝐴)) ∧ 𝑋 No ) → (( bday 𝑋) ⊆ 𝐴𝑋 ∈ ( M ‘𝐴)))
7670, 75sylan 581 . 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 397  wo 846   = wceq 1542  wcel 2107  wral 3062  wss 3949   class class class wbr 5149  Oncon0 6365  cfv 6544  (class class class)co 7409   No csur 27143   bday cbday 27145   <<s csslt 27282   |s cscut 27284   M cmade 27337   O cold 27338   L cleft 27340   R cright 27341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-1o 8466  df-2o 8467  df-no 27146  df-slt 27147  df-bday 27148  df-sslt 27283  df-scut 27285  df-made 27342  df-old 27343  df-left 27345  df-right 27346
This theorem is referenced by:  oldbday  27395  newbday  27396  lrcut  27397
  Copyright terms: Public domain W3C validator