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 X M A bday X A

Proof

Step Hyp Ref Expression
1 elfvdm X M A A dom M
2 madef M : On 𝒫 No
3 2 fdmi dom M = On
4 1 3 eleqtrdi X M A A On
5 fveq2 a = b M a = M b
6 sseq2 a = b bday x a bday x b
7 5 6 raleqbidv a = b x M a bday x a x M b bday x b
8 fveq2 x = y bday x = bday y
9 8 sseq1d x = y bday x b bday y b
10 9 cbvralvw x M b bday x b y M b bday y b
11 7 10 bitrdi a = b x M a bday x a y M b bday y b
12 fveq2 a = A M a = M A
13 sseq2 a = A bday x a bday x A
14 12 13 raleqbidv a = A x M a bday x a x M A bday x A
15 elmade2 a On x M a l 𝒫 Old a r 𝒫 Old a l s r l | s r = x
16 15 adantr a On b a y M b bday y b x M a l 𝒫 Old a r 𝒫 Old a l s r l | s r = x
17 elpwi l 𝒫 Old a l Old a
18 elpwi r 𝒫 Old a r Old a
19 17 18 anim12i l 𝒫 Old a r 𝒫 Old a l Old a r Old a
20 unss l Old a r Old a l r Old a
21 19 20 sylib l 𝒫 Old a r 𝒫 Old a l r Old a
22 simpr a On b a y M b bday y b l r Old a l s r l s r
23 simplll a On b a y M b bday y b l r Old a l s r a On
24 dfss3 l r Old a z l r z Old a
25 fveq2 y = z bday y = bday z
26 25 sseq1d y = z bday y b bday z b
27 26 rspccv y M b bday y b z M b bday z b
28 27 ralimi b a y M b bday y b b a z M b bday z b
29 rexim b a z M b bday z b b a z M b b a bday z b
30 28 29 syl b a y M b bday y b b a z M b b a bday z b
31 30 adantl a On b a y M b bday y b b a z M b b a bday z b
32 elold a On z Old a b a z M b
33 32 adantr a On b a y M b bday y b z Old a b a z M b
34 bdayelon bday z On
35 onelssex bday z On a On bday z a b a bday z b
36 34 35 mpan a On bday z a b a bday z b
37 36 adantr a On b a y M b bday y b bday z a b a bday z b
38 31 33 37 3imtr4d a On b a y M b bday y b z Old a bday z a
39 38 ralimdv a On b a y M b bday y b z l r z Old a z l r bday z a
40 24 39 syl5bi a On b a y M b bday y b l r Old a z l r bday z a
41 40 imp a On b a y M b bday y b l r Old a z l r bday z a
42 41 adantr a On b a y M b bday y b l r Old a l s r z l r bday z a
43 bdayfun Fun bday
44 oldssno Old a No
45 sstr l r Old a Old a No l r No
46 44 45 mpan2 l r Old a l r No
47 bdaydm dom bday = No
48 46 47 sseqtrrdi l r Old a l r dom bday
49 funimass4 Fun bday l r dom bday bday l r a z l r bday z a
50 43 48 49 sylancr l r Old a bday l r a z l r bday z a
51 50 adantl a On b a y M b bday y b l r Old a bday l r a z l r bday z a
52 51 adantr a On b a y M b bday y b l r Old a l s r bday l r a z l r bday z a
53 42 52 mpbird a On b a y M b bday y b l r Old a l s r bday l r a
54 scutbdaybnd l s r a On bday l r a bday l | s r a
55 22 23 53 54 syl3anc a On b a y M b bday y b l r Old a l s r bday l | s r a
56 fveq2 l | s r = x bday l | s r = bday x
57 56 sseq1d l | s r = x bday l | s r a bday x a
58 55 57 syl5ibcom a On b a y M b bday y b l r Old a l s r l | s r = x bday x a
59 58 expimpd a On b a y M b bday y b l r Old a l s r l | s r = x bday x a
60 59 ex a On b a y M b bday y b l r Old a l s r l | s r = x bday x a
61 21 60 syl5 a On b a y M b bday y b l 𝒫 Old a r 𝒫 Old a l s r l | s r = x bday x a
62 61 rexlimdvv a On b a y M b bday y b l 𝒫 Old a r 𝒫 Old a l s r l | s r = x bday x a
63 16 62 sylbid a On b a y M b bday y b x M a bday x a
64 63 ralrimiv a On b a y M b bday y b x M a bday x a
65 64 ex a On b a y M b bday y b x M a bday x a
66 11 14 65 tfis3 A On x M A bday x A
67 fveq2 x = X bday x = bday X
68 67 sseq1d x = X bday x A bday X A
69 68 rspccv x M A bday x A X M A bday X A
70 66 69 syl A On X M A bday X A
71 4 70 mpcom X M A bday X A