Metamath Proof Explorer


Theorem madebday

Description: A surreal is part of the set made by ordinal A iff its birthday is less than or equal to A . Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebday ( ( 𝐴 ∈ On ∧ 𝑋 No ) → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ( bday 𝑋 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 madebdayim ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday 𝑋 ) ⊆ 𝐴 )
2 sseq2 ( 𝑎 = 𝑏 → ( ( bday 𝑥 ) ⊆ 𝑎 ↔ ( bday 𝑥 ) ⊆ 𝑏 ) )
3 fveq2 ( 𝑎 = 𝑏 → ( M ‘ 𝑎 ) = ( M ‘ 𝑏 ) )
4 3 eleq2d ( 𝑎 = 𝑏 → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ 𝑥 ∈ ( M ‘ 𝑏 ) ) )
5 2 4 imbi12d ( 𝑎 = 𝑏 → ( ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ( ( bday 𝑥 ) ⊆ 𝑏𝑥 ∈ ( M ‘ 𝑏 ) ) ) )
6 5 ralbidv ( 𝑎 = 𝑏 → ( ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑏𝑥 ∈ ( M ‘ 𝑏 ) ) ) )
7 fveq2 ( 𝑥 = 𝑦 → ( bday 𝑥 ) = ( bday 𝑦 ) )
8 7 sseq1d ( 𝑥 = 𝑦 → ( ( bday 𝑥 ) ⊆ 𝑏 ↔ ( bday 𝑦 ) ⊆ 𝑏 ) )
9 eleq1 ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( M ‘ 𝑏 ) ↔ 𝑦 ∈ ( M ‘ 𝑏 ) ) )
10 8 9 imbi12d ( 𝑥 = 𝑦 → ( ( ( bday 𝑥 ) ⊆ 𝑏𝑥 ∈ ( M ‘ 𝑏 ) ) ↔ ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) )
11 10 cbvralvw ( ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑏𝑥 ∈ ( M ‘ 𝑏 ) ) ↔ ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) )
12 6 11 bitrdi ( 𝑎 = 𝑏 → ( ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) )
13 sseq2 ( 𝑎 = 𝐴 → ( ( bday 𝑥 ) ⊆ 𝑎 ↔ ( bday 𝑥 ) ⊆ 𝐴 ) )
14 fveq2 ( 𝑎 = 𝐴 → ( M ‘ 𝑎 ) = ( M ‘ 𝐴 ) )
15 14 eleq2d ( 𝑎 = 𝐴 → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ 𝑥 ∈ ( M ‘ 𝐴 ) ) )
16 13 15 imbi12d ( 𝑎 = 𝐴 → ( ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ( ( bday 𝑥 ) ⊆ 𝐴𝑥 ∈ ( M ‘ 𝐴 ) ) ) )
17 16 ralbidv ( 𝑎 = 𝐴 → ( ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝐴𝑥 ∈ ( M ‘ 𝐴 ) ) ) )
18 bdayelon ( bday 𝑥 ) ∈ On
19 onsseleq ( ( ( bday 𝑥 ) ∈ On ∧ 𝑎 ∈ On ) → ( ( bday 𝑥 ) ⊆ 𝑎 ↔ ( ( bday 𝑥 ) ∈ 𝑎 ∨ ( bday 𝑥 ) = 𝑎 ) ) )
20 18 19 mpan ( 𝑎 ∈ On → ( ( bday 𝑥 ) ⊆ 𝑎 ↔ ( ( bday 𝑥 ) ∈ 𝑎 ∨ ( bday 𝑥 ) = 𝑎 ) ) )
21 20 ad2antrr ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → ( ( bday 𝑥 ) ⊆ 𝑎 ↔ ( ( bday 𝑥 ) ∈ 𝑎 ∨ ( bday 𝑥 ) = 𝑎 ) ) )
22 simpll ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → 𝑎 ∈ On )
23 onelss ( 𝑎 ∈ On → ( ( bday 𝑥 ) ∈ 𝑎 → ( bday 𝑥 ) ⊆ 𝑎 ) )
24 23 ad2antrr ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → ( ( bday 𝑥 ) ∈ 𝑎 → ( bday 𝑥 ) ⊆ 𝑎 ) )
25 24 imp ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → ( bday 𝑥 ) ⊆ 𝑎 )
26 madess ( ( 𝑎 ∈ On ∧ ( bday 𝑥 ) ⊆ 𝑎 ) → ( M ‘ ( bday 𝑥 ) ) ⊆ ( M ‘ 𝑎 ) )
27 22 25 26 syl2an2r ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → ( M ‘ ( bday 𝑥 ) ) ⊆ ( M ‘ 𝑎 ) )
28 ssid ( bday 𝑥 ) ⊆ ( bday 𝑥 )
29 simpr ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → ( bday 𝑥 ) ∈ 𝑎 )
30 simplr ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → 𝑥 No )
31 29 30 jca ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → ( ( bday 𝑥 ) ∈ 𝑎𝑥 No ) )
32 simpllr ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) )
33 sseq2 ( 𝑏 = ( bday 𝑥 ) → ( ( bday 𝑦 ) ⊆ 𝑏 ↔ ( bday 𝑦 ) ⊆ ( bday 𝑥 ) ) )
34 fveq2 ( 𝑏 = ( bday 𝑥 ) → ( M ‘ 𝑏 ) = ( M ‘ ( bday 𝑥 ) ) )
35 34 eleq2d ( 𝑏 = ( bday 𝑥 ) → ( 𝑦 ∈ ( M ‘ 𝑏 ) ↔ 𝑦 ∈ ( M ‘ ( bday 𝑥 ) ) ) )
36 33 35 imbi12d ( 𝑏 = ( bday 𝑥 ) → ( ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ↔ ( ( bday 𝑦 ) ⊆ ( bday 𝑥 ) → 𝑦 ∈ ( M ‘ ( bday 𝑥 ) ) ) ) )
37 fveq2 ( 𝑦 = 𝑥 → ( bday 𝑦 ) = ( bday 𝑥 ) )
38 37 sseq1d ( 𝑦 = 𝑥 → ( ( bday 𝑦 ) ⊆ ( bday 𝑥 ) ↔ ( bday 𝑥 ) ⊆ ( bday 𝑥 ) ) )
39 eleq1 ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( M ‘ ( bday 𝑥 ) ) ↔ 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) ) )
40 38 39 imbi12d ( 𝑦 = 𝑥 → ( ( ( bday 𝑦 ) ⊆ ( bday 𝑥 ) → 𝑦 ∈ ( M ‘ ( bday 𝑥 ) ) ) ↔ ( ( bday 𝑥 ) ⊆ ( bday 𝑥 ) → 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) ) ) )
41 36 40 rspc2v ( ( ( bday 𝑥 ) ∈ 𝑎𝑥 No ) → ( ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) → ( ( bday 𝑥 ) ⊆ ( bday 𝑥 ) → 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) ) ) )
42 31 32 41 sylc ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → ( ( bday 𝑥 ) ⊆ ( bday 𝑥 ) → 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) ) )
43 28 42 mpi ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) )
44 27 43 sseldd ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) ∧ ( bday 𝑥 ) ∈ 𝑎 ) → 𝑥 ∈ ( M ‘ 𝑎 ) )
45 44 ex ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → ( ( bday 𝑥 ) ∈ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) )
46 madebdaylemlrcut ( ( ∀ 𝑏 ∈ ( bday 𝑥 ) ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
47 18 a1i ( 𝑥 No → ( bday 𝑥 ) ∈ On )
48 lltropt ( 𝑥 No → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) )
49 leftssold ( L ‘ 𝑥 ) ⊆ ( O ‘ ( bday 𝑥 ) )
50 49 a1i ( 𝑥 No → ( L ‘ 𝑥 ) ⊆ ( O ‘ ( bday 𝑥 ) ) )
51 rightssold ( R ‘ 𝑥 ) ⊆ ( O ‘ ( bday 𝑥 ) )
52 51 a1i ( 𝑥 No → ( R ‘ 𝑥 ) ⊆ ( O ‘ ( bday 𝑥 ) ) )
53 madecut ( ( ( ( bday 𝑥 ) ∈ On ∧ ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) ) ∧ ( ( L ‘ 𝑥 ) ⊆ ( O ‘ ( bday 𝑥 ) ) ∧ ( R ‘ 𝑥 ) ⊆ ( O ‘ ( bday 𝑥 ) ) ) ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∈ ( M ‘ ( bday 𝑥 ) ) )
54 47 48 50 52 53 syl22anc ( 𝑥 No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∈ ( M ‘ ( bday 𝑥 ) ) )
55 54 adantl ( ( ∀ 𝑏 ∈ ( bday 𝑥 ) ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∈ ( M ‘ ( bday 𝑥 ) ) )
56 46 55 eqeltrrd ( ( ∀ 𝑏 ∈ ( bday 𝑥 ) ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) )
57 raleq ( ( bday 𝑥 ) = 𝑎 → ( ∀ 𝑏 ∈ ( bday 𝑥 ) ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ↔ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) )
58 57 anbi1d ( ( bday 𝑥 ) = 𝑎 → ( ( ∀ 𝑏 ∈ ( bday 𝑥 ) ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) ↔ ( ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) ) )
59 fveq2 ( ( bday 𝑥 ) = 𝑎 → ( M ‘ ( bday 𝑥 ) ) = ( M ‘ 𝑎 ) )
60 59 eleq2d ( ( bday 𝑥 ) = 𝑎 → ( 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) ↔ 𝑥 ∈ ( M ‘ 𝑎 ) ) )
61 58 60 imbi12d ( ( bday 𝑥 ) = 𝑎 → ( ( ( ∀ 𝑏 ∈ ( bday 𝑥 ) ∀ 𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘ ( bday 𝑥 ) ) ) ↔ ( ( ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘ 𝑎 ) ) ) )
62 56 61 mpbii ( ( bday 𝑥 ) = 𝑎 → ( ( ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
63 62 com12 ( ( ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 No ) → ( ( bday 𝑥 ) = 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) )
64 63 adantll ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → ( ( bday 𝑥 ) = 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) )
65 45 64 jaod ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → ( ( ( bday 𝑥 ) ∈ 𝑎 ∨ ( bday 𝑥 ) = 𝑎 ) → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
66 21 65 sylbid ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 No ) → ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) )
67 66 ralrimiva ( ( 𝑎 ∈ On ∧ ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) ) → ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) )
68 67 ex ( 𝑎 ∈ On → ( ∀ 𝑏𝑎𝑦 No ( ( bday 𝑦 ) ⊆ 𝑏𝑦 ∈ ( M ‘ 𝑏 ) ) → ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝑎𝑥 ∈ ( M ‘ 𝑎 ) ) ) )
69 12 17 68 tfis3 ( 𝐴 ∈ On → ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝐴𝑥 ∈ ( M ‘ 𝐴 ) ) )
70 fveq2 ( 𝑥 = 𝑋 → ( bday 𝑥 ) = ( bday 𝑋 ) )
71 70 sseq1d ( 𝑥 = 𝑋 → ( ( bday 𝑥 ) ⊆ 𝐴 ↔ ( bday 𝑋 ) ⊆ 𝐴 ) )
72 eleq1 ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( M ‘ 𝐴 ) ↔ 𝑋 ∈ ( M ‘ 𝐴 ) ) )
73 71 72 imbi12d ( 𝑥 = 𝑋 → ( ( ( bday 𝑥 ) ⊆ 𝐴𝑥 ∈ ( M ‘ 𝐴 ) ) ↔ ( ( bday 𝑋 ) ⊆ 𝐴𝑋 ∈ ( M ‘ 𝐴 ) ) ) )
74 73 rspccva ( ( ∀ 𝑥 No ( ( bday 𝑥 ) ⊆ 𝐴𝑥 ∈ ( M ‘ 𝐴 ) ) ∧ 𝑋 No ) → ( ( bday 𝑋 ) ⊆ 𝐴𝑋 ∈ ( M ‘ 𝐴 ) ) )
75 69 74 sylan ( ( 𝐴 ∈ On ∧ 𝑋 No ) → ( ( bday 𝑋 ) ⊆ 𝐴𝑋 ∈ ( M ‘ 𝐴 ) ) )
76 1 75 impbid2 ( ( 𝐴 ∈ On ∧ 𝑋 No ) → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ( bday 𝑋 ) ⊆ 𝐴 ) )