Metamath Proof Explorer

Theorem madebdayim

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)

Ref Expression
Assertion madebdayim ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → 𝐴 ∈ dom M )
2 madef ⊢ M : On ⟶ 𝒫 No
3 2 fdmi ⊢ dom M = On
4 1 3 eleqtrdi ⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → 𝐴 ∈ On )
5 fveq2 ⊢ ( 𝑎 = 𝑏 → ( M ‘ 𝑎 ) = ( M ‘ 𝑏 ) )
6 sseq2 ⊢ ( 𝑎 = 𝑏 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑏 ) )
7 5 6 raleqbidv ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑥 ) ⊆ 𝑏 ) )
8 fveq2 ⊢ ( 𝑥 = 𝑦 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) )
9 8 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) )
10 9 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 )
11 7 10 bitrdi ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) )
12 fveq2 ⊢ ( 𝑎 = 𝐴 → ( M ‘ 𝑎 ) = ( M ‘ 𝐴 ) )
13 sseq2 ⊢ ( 𝑎 = 𝐴 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝐴 ) )
14 12 13 raleqbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 ) )
15 elmade2 ⊢ ( 𝑎 ∈ On → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
16 15 adantr ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
17 elpwi ⊢ ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) → 𝑙 ⊆ ( O ‘ 𝑎 ) )
18 elpwi ⊢ ( 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) → 𝑟 ⊆ ( O ‘ 𝑎 ) )
19 17 18 anim12i ⊢ ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( 𝑙 ⊆ ( O ‘ 𝑎 ) ∧ 𝑟 ⊆ ( O ‘ 𝑎 ) ) )
20 unss ⊢ ( ( 𝑙 ⊆ ( O ‘ 𝑎 ) ∧ 𝑟 ⊆ ( O ‘ 𝑎 ) ) ↔ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) )
21 19 20 sylib ⊢ ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) )
22 simpr ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → 𝑙 <<s 𝑟 )
23 simplll ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → 𝑎 ∈ On )
24 dfss3 ⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) 𝑧 ∈ ( O ‘ 𝑎 ) )
25 fveq2 ⊢ ( 𝑦 = 𝑧 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑧 ) )
26 25 sseq1d ⊢ ( 𝑦 = 𝑧 → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
27 26 rspccv ⊢ ( ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
28 27 ralimi ⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ∀ 𝑏 ∈ 𝑎 ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
29 rexim ⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
30 28 29 syl ⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
31 30 adantl ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
32 elold ⊢ ( 𝑎 ∈ On → ( 𝑧 ∈ ( O ‘ 𝑎 ) ↔ ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) ) )
33 32 adantr ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑧 ∈ ( O ‘ 𝑎 ) ↔ ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) ) )
34 bdayelon ⊢ ( bday ‘ 𝑧 ) ∈ On
35 onelssex ⊢ ( ( ( bday ‘ 𝑧 ) ∈ On ∧ 𝑎 ∈ On ) → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
36 34 35 mpan ⊢ ( 𝑎 ∈ On → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
37 36 adantr ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) )
38 31 33 37 3imtr4d ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑧 ∈ ( O ‘ 𝑎 ) → ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
39 38 ralimdv ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) 𝑧 ∈ ( O ‘ 𝑎 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
40 24 39 syl5bi ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
41 40 imp ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 )
42 41 adantr ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 )
43 bdayfun ⊢ Fun bday
44 oldssno ⊢ ( O ‘ 𝑎 ) ⊆ No
45 sstr ⊢ ( ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ ( O ‘ 𝑎 ) ⊆ No ) → ( 𝑙 ∪ 𝑟 ) ⊆ No )
46 44 45 mpan2 ⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( 𝑙 ∪ 𝑟 ) ⊆ No )
47 bdaydm ⊢ dom bday = No
48 46 47 sseqtrrdi ⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( 𝑙 ∪ 𝑟 ) ⊆ dom bday )
49 funimass4 ⊢ ( ( Fun bday ∧ ( 𝑙 ∪ 𝑟 ) ⊆ dom bday ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
50 43 48 49 sylancr ⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
51 50 adantl ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
52 51 adantr ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) )
53 42 52 mpbird ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 )
54 scutbdaybnd ⊢ ( ( 𝑙 <<s 𝑟 ∧ 𝑎 ∈ On ∧ ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ) → ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 )
55 22 23 53 54 syl3anc ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 )
56 fveq2 ⊢ ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ ( 𝑙 |s 𝑟 ) ) = ( bday ‘ 𝑥 ) )
57 56 sseq1d ⊢ ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
58 55 57 syl5ibcom ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
59 58 expimpd ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
60 59 ex ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) )
61 21 60 syl5 ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) )
62 61 rexlimdvv ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
63 16 62 sylbid ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑥 ∈ ( M ‘ 𝑎 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
64 63 ralrimiv ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 )
65 64 ex ⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
66 11 14 65 tfis3 ⊢ ( 𝐴 ∈ On → ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 )
67 fveq2 ⊢ ( 𝑥 = 𝑋 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑋 ) )
68 67 sseq1d ⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) ⊆ 𝐴 ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )
69 68 rspccv ⊢ ( ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 → ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )
70 66 69 syl ⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )
71 4 70 mpcom ⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 )