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 ⊢ A ∈ On ∧ X ∈ No → X ∈ M ⁡ A ↔ bday ⁡ X ⊆ A

Proof

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