Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  madebdayim Structured version   Visualization version   GIF version

 Description: If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024.)
Assertion
Ref Expression
madebdayim ((𝐴 ∈ On ∧ 𝑋 ∈ ( M ‘𝐴)) → ( bday 𝑋) ⊆ 𝐴)

Dummy variables 𝑎 𝑏 𝑥 𝑦 𝑧 𝑙 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6663 . . . . 5 (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏))
2 sseq2 3920 . . . . 5 (𝑎 = 𝑏 → (( bday 𝑥) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝑏))
31, 2raleqbidv 3319 . . . 4 (𝑎 = 𝑏 → (∀𝑥 ∈ ( M ‘𝑎)( bday 𝑥) ⊆ 𝑎 ↔ ∀𝑥 ∈ ( M ‘𝑏)( bday 𝑥) ⊆ 𝑏))
4 fveq2 6663 . . . . . 6 (𝑥 = 𝑦 → ( bday 𝑥) = ( bday 𝑦))
54sseq1d 3925 . . . . 5 (𝑥 = 𝑦 → (( bday 𝑥) ⊆ 𝑏 ↔ ( bday 𝑦) ⊆ 𝑏))
65cbvralvw 3361 . . . 4 (∀𝑥 ∈ ( M ‘𝑏)( bday 𝑥) ⊆ 𝑏 ↔ ∀𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏)
73, 6bitrdi 290 . . 3 (𝑎 = 𝑏 → (∀𝑥 ∈ ( M ‘𝑎)( bday 𝑥) ⊆ 𝑎 ↔ ∀𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏))
8 fveq2 6663 . . . 4 (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴))
9 sseq2 3920 . . . 4 (𝑎 = 𝐴 → (( bday 𝑥) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝐴))
108, 9raleqbidv 3319 . . 3 (𝑎 = 𝐴 → (∀𝑥 ∈ ( M ‘𝑎)( bday 𝑥) ⊆ 𝑎 ↔ ∀𝑥 ∈ ( M ‘𝐴)( bday 𝑥) ⊆ 𝐴))
11 elmade2 33642 . . . . . . 7 (𝑎 ∈ On → (𝑥 ∈ ( M ‘𝑎) ↔ ∃𝑙 ∈ 𝒫 ( O ‘𝑎)∃𝑟 ∈ 𝒫 ( O ‘𝑎)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)))
1211adantr 484 . . . . . 6 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (𝑥 ∈ ( M ‘𝑎) ↔ ∃𝑙 ∈ 𝒫 ( O ‘𝑎)∃𝑟 ∈ 𝒫 ( O ‘𝑎)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)))
13 pwuncl 7497 . . . . . . . . 9 ((𝑙 ∈ 𝒫 ( O ‘𝑎) ∧ 𝑟 ∈ 𝒫 ( O ‘𝑎)) → (𝑙𝑟) ∈ 𝒫 ( O ‘𝑎))
1413elpwid 4508 . . . . . . . 8 ((𝑙 ∈ 𝒫 ( O ‘𝑎) ∧ 𝑟 ∈ 𝒫 ( O ‘𝑎)) → (𝑙𝑟) ⊆ ( O ‘𝑎))
15 simprr 772 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → 𝑙 <<s 𝑟)
16 simpll 766 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → 𝑎 ∈ On)
17 dfss3 3882 . . . . . . . . . . . . . . . . 17 ((𝑙𝑟) ⊆ ( O ‘𝑎) ↔ ∀𝑧 ∈ (𝑙𝑟)𝑧 ∈ ( O ‘𝑎))
18 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ( bday 𝑦) = ( bday 𝑧))
1918sseq1d 3925 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → (( bday 𝑦) ⊆ 𝑏 ↔ ( bday 𝑧) ⊆ 𝑏))
2019rspccv 3540 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏 → (𝑧 ∈ ( M ‘𝑏) → ( bday 𝑧) ⊆ 𝑏))
2120ralimi 3092 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏 → ∀𝑏𝑎 (𝑧 ∈ ( M ‘𝑏) → ( bday 𝑧) ⊆ 𝑏))
22 rexim 3168 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑏𝑎 (𝑧 ∈ ( M ‘𝑏) → ( bday 𝑧) ⊆ 𝑏) → (∃𝑏𝑎 𝑧 ∈ ( M ‘𝑏) → ∃𝑏𝑎 ( bday 𝑧) ⊆ 𝑏))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . 20 (∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏 → (∃𝑏𝑎 𝑧 ∈ ( M ‘𝑏) → ∃𝑏𝑎 ( bday 𝑧) ⊆ 𝑏))
2423adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (∃𝑏𝑎 𝑧 ∈ ( M ‘𝑏) → ∃𝑏𝑎 ( bday 𝑧) ⊆ 𝑏))
25 elold 33643 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → (𝑧 ∈ ( O ‘𝑎) ↔ ∃𝑏𝑎 𝑧 ∈ ( M ‘𝑏)))
2625adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (𝑧 ∈ ( O ‘𝑎) ↔ ∃𝑏𝑎 𝑧 ∈ ( M ‘𝑏)))
27 bdayelon 33568 . . . . . . . . . . . . . . . . . . . . 21 ( bday 𝑧) ∈ On
28 onelssex 33191 . . . . . . . . . . . . . . . . . . . . 21 ((( bday 𝑧) ∈ On ∧ 𝑎 ∈ On) → (( bday 𝑧) ∈ 𝑎 ↔ ∃𝑏𝑎 ( bday 𝑧) ⊆ 𝑏))
2927, 28mpan 689 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → (( bday 𝑧) ∈ 𝑎 ↔ ∃𝑏𝑎 ( bday 𝑧) ⊆ 𝑏))
3029adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (( bday 𝑧) ∈ 𝑎 ↔ ∃𝑏𝑎 ( bday 𝑧) ⊆ 𝑏))
3124, 26, 303imtr4d 297 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (𝑧 ∈ ( O ‘𝑎) → ( bday 𝑧) ∈ 𝑎))
3231ralimdv 3109 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (∀𝑧 ∈ (𝑙𝑟)𝑧 ∈ ( O ‘𝑎) → ∀𝑧 ∈ (𝑙𝑟)( bday 𝑧) ∈ 𝑎))
3317, 32syl5bi 245 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → ((𝑙𝑟) ⊆ ( O ‘𝑎) → ∀𝑧 ∈ (𝑙𝑟)( bday 𝑧) ∈ 𝑎))
3433imp 410 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ (𝑙𝑟) ⊆ ( O ‘𝑎)) → ∀𝑧 ∈ (𝑙𝑟)( bday 𝑧) ∈ 𝑎)
3534adantrr 716 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → ∀𝑧 ∈ (𝑙𝑟)( bday 𝑧) ∈ 𝑎)
36 bdayfun 33564 . . . . . . . . . . . . . . 15 Fun bday
37 ssltss1 33580 . . . . . . . . . . . . . . . . . . 19 (𝑙 <<s 𝑟𝑙 No )
38 ssltss2 33581 . . . . . . . . . . . . . . . . . . 19 (𝑙 <<s 𝑟𝑟 No )
3937, 38unssd 4093 . . . . . . . . . . . . . . . . . 18 (𝑙 <<s 𝑟 → (𝑙𝑟) ⊆ No )
4039adantl 485 . . . . . . . . . . . . . . . . 17 (((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟) → (𝑙𝑟) ⊆ No )
4140adantl 485 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → (𝑙𝑟) ⊆ No )
42 bdaydm 33566 . . . . . . . . . . . . . . . 16 dom bday = No
4341, 42sseqtrrdi 3945 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → (𝑙𝑟) ⊆ dom bday )
44 funimass4 6723 . . . . . . . . . . . . . . 15 ((Fun bday ∧ (𝑙𝑟) ⊆ dom bday ) → (( bday “ (𝑙𝑟)) ⊆ 𝑎 ↔ ∀𝑧 ∈ (𝑙𝑟)( bday 𝑧) ∈ 𝑎))
4536, 43, 44sylancr 590 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → (( bday “ (𝑙𝑟)) ⊆ 𝑎 ↔ ∀𝑧 ∈ (𝑙𝑟)( bday 𝑧) ∈ 𝑎))
4635, 45mpbird 260 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → ( bday “ (𝑙𝑟)) ⊆ 𝑎)
47 scutbdaybnd 33604 . . . . . . . . . . . . 13 ((𝑙 <<s 𝑟𝑎 ∈ On ∧ ( bday “ (𝑙𝑟)) ⊆ 𝑎) → ( bday ‘(𝑙 |s 𝑟)) ⊆ 𝑎)
4815, 16, 46, 47syl3anc 1368 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → ( bday ‘(𝑙 |s 𝑟)) ⊆ 𝑎)
49 fveq2 6663 . . . . . . . . . . . . 13 ((𝑙 |s 𝑟) = 𝑥 → ( bday ‘(𝑙 |s 𝑟)) = ( bday 𝑥))
5049sseq1d 3925 . . . . . . . . . . . 12 ((𝑙 |s 𝑟) = 𝑥 → (( bday ‘(𝑙 |s 𝑟)) ⊆ 𝑎 ↔ ( bday 𝑥) ⊆ 𝑎))
5148, 50syl5ibcom 248 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ ((𝑙𝑟) ⊆ ( O ‘𝑎) ∧ 𝑙 <<s 𝑟)) → ((𝑙 |s 𝑟) = 𝑥 → ( bday 𝑥) ⊆ 𝑎))
5251expr 460 . . . . . . . . . 10 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ (𝑙𝑟) ⊆ ( O ‘𝑎)) → (𝑙 <<s 𝑟 → ((𝑙 |s 𝑟) = 𝑥 → ( bday 𝑥) ⊆ 𝑎)))
5352impd 414 . . . . . . . . 9 (((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) ∧ (𝑙𝑟) ⊆ ( O ‘𝑎)) → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday 𝑥) ⊆ 𝑎))
5453ex 416 . . . . . . . 8 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → ((𝑙𝑟) ⊆ ( O ‘𝑎) → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday 𝑥) ⊆ 𝑎)))
5514, 54syl5 34 . . . . . . 7 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → ((𝑙 ∈ 𝒫 ( O ‘𝑎) ∧ 𝑟 ∈ 𝒫 ( O ‘𝑎)) → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday 𝑥) ⊆ 𝑎)))
5655rexlimdvv 3217 . . . . . 6 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (∃𝑙 ∈ 𝒫 ( O ‘𝑎)∃𝑟 ∈ 𝒫 ( O ‘𝑎)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday 𝑥) ⊆ 𝑎))
5712, 56sylbid 243 . . . . 5 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → (𝑥 ∈ ( M ‘𝑎) → ( bday 𝑥) ⊆ 𝑎))
5857ralrimiv 3112 . . . 4 ((𝑎 ∈ On ∧ ∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏) → ∀𝑥 ∈ ( M ‘𝑎)( bday 𝑥) ⊆ 𝑎)
5958ex 416 . . 3 (𝑎 ∈ On → (∀𝑏𝑎𝑦 ∈ ( M ‘𝑏)( bday 𝑦) ⊆ 𝑏 → ∀𝑥 ∈ ( M ‘𝑎)( bday 𝑥) ⊆ 𝑎))
607, 10, 59tfis3 7577 . 2 (𝐴 ∈ On → ∀𝑥 ∈ ( M ‘𝐴)( bday 𝑥) ⊆ 𝐴)
61 fveq2 6663 . . . 4 (𝑥 = 𝑋 → ( bday 𝑥) = ( bday 𝑋))
6261sseq1d 3925 . . 3 (𝑥 = 𝑋 → (( bday 𝑥) ⊆ 𝐴 ↔ ( bday 𝑋) ⊆ 𝐴))
6362rspccva 3542 . 2 ((∀𝑥 ∈ ( M ‘𝐴)( bday 𝑥) ⊆ 𝐴𝑋 ∈ ( M ‘𝐴)) → ( bday 𝑋) ⊆ 𝐴)
6460, 63sylan 583 1 ((𝐴 ∈ On ∧ 𝑋 ∈ ( M ‘𝐴)) → ( bday 𝑋) ⊆ 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071   ∪ cun 3858   ⊆ wss 3860  𝒫 cpw 4497   class class class wbr 5036  dom cdm 5528   “ cima 5531  Oncon0 6174  Fun wfun 6334  ‘cfv 6340  (class class class)co 7156   No csur 33440   bday cbday 33442   <
 Copyright terms: Public domain W3C validator