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 ⊢ A ∈ On ∧ X ∈ M ⁡ A → bday ⁡ X ⊆ A
2 1 ex ⊢ A ∈ On → X ∈ M ⁡ A → bday ⁡ X ⊆ A
3 2 adantr ⊢ A ∈ On ∧ X ∈ No → X ∈ M ⁡ A → bday ⁡ X ⊆ A
4 sseq2 ⊢ a = b → bday ⁡ x ⊆ a ↔ bday ⁡ x ⊆ b
5 fveq2 ⊢ a = b → M ⁡ a = M ⁡ b
6 5 eleq2d ⊢ a = b → x ∈ M ⁡ a ↔ x ∈ M ⁡ b
7 4 6 imbi12d ⊢ a = b → bday ⁡ x ⊆ a → x ∈ M ⁡ a ↔ bday ⁡ x ⊆ b → x ∈ M ⁡ b
8 7 ralbidv ⊢ a = b → ∀ x ∈ No bday ⁡ x ⊆ a → x ∈ M ⁡ a ↔ ∀ x ∈ No bday ⁡ x ⊆ b → x ∈ M ⁡ b
9 fveq2 ⊢ x = y → bday ⁡ x = bday ⁡ y
10 9 sseq1d ⊢ x = y → bday ⁡ x ⊆ b ↔ bday ⁡ y ⊆ b
11 eleq1 ⊢ x = y → x ∈ M ⁡ b ↔ y ∈ M ⁡ b
12 10 11 imbi12d ⊢ x = y → bday ⁡ x ⊆ b → x ∈ M ⁡ b ↔ bday ⁡ y ⊆ b → y ∈ M ⁡ b
13 12 cbvralvw ⊢ ∀ x ∈ No bday ⁡ x ⊆ b → x ∈ M ⁡ b ↔ ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
14 8 13 bitrdi ⊢ a = b → ∀ x ∈ No bday ⁡ x ⊆ a → x ∈ M ⁡ a ↔ ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
15 sseq2 ⊢ a = A → bday ⁡ x ⊆ a ↔ bday ⁡ x ⊆ A
16 fveq2 ⊢ a = A → M ⁡ a = M ⁡ A
17 16 eleq2d ⊢ a = A → x ∈ M ⁡ a ↔ x ∈ M ⁡ A
18 15 17 imbi12d ⊢ a = A → bday ⁡ x ⊆ a → x ∈ M ⁡ a ↔ bday ⁡ x ⊆ A → x ∈ M ⁡ A
19 18 ralbidv ⊢ a = A → ∀ x ∈ No bday ⁡ x ⊆ a → x ∈ M ⁡ a ↔ ∀ x ∈ No bday ⁡ x ⊆ A → x ∈ M ⁡ A
20 bdayelon ⊢ bday ⁡ x ∈ On
21 onsseleq ⊢ bday ⁡ x ∈ On ∧ a ∈ On → bday ⁡ x ⊆ a ↔ bday ⁡ x ∈ a ∨ bday ⁡ x = a
22 20 21 mpan ⊢ a ∈ On → bday ⁡ x ⊆ a ↔ bday ⁡ x ∈ a ∨ bday ⁡ x = a
23 22 ad2antrr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No → bday ⁡ x ⊆ a ↔ bday ⁡ x ∈ a ∨ bday ⁡ x = a
24 simpll ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No → a ∈ On
25 onelss ⊢ a ∈ On → bday ⁡ x ∈ a → bday ⁡ x ⊆ a
26 25 ad2antrr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No → bday ⁡ x ∈ a → bday ⁡ x ⊆ a
27 26 imp ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → bday ⁡ x ⊆ a
28 madess ⊢ bday ⁡ x ∈ On ∧ a ∈ On ∧ bday ⁡ x ⊆ a → M ⁡ bday ⁡ x ⊆ M ⁡ a
29 20 24 27 28 mp3an2ani ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → M ⁡ bday ⁡ x ⊆ M ⁡ a
30 ssid ⊢ bday ⁡ x ⊆ bday ⁡ x
31 simpr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → bday ⁡ x ∈ a
32 simplr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → x ∈ No
33 31 32 jca ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → bday ⁡ x ∈ a ∧ x ∈ No
34 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
35 sseq2 ⊢ b = bday ⁡ x → bday ⁡ y ⊆ b ↔ bday ⁡ y ⊆ bday ⁡ x
36 fveq2 ⊢ b = bday ⁡ x → M ⁡ b = M ⁡ bday ⁡ x
37 36 eleq2d ⊢ b = bday ⁡ x → y ∈ M ⁡ b ↔ y ∈ M ⁡ bday ⁡ x
38 35 37 imbi12d ⊢ b = bday ⁡ x → bday ⁡ y ⊆ b → y ∈ M ⁡ b ↔ bday ⁡ y ⊆ bday ⁡ x → y ∈ M ⁡ bday ⁡ x
39 fveq2 ⊢ y = x → bday ⁡ y = bday ⁡ x
40 39 sseq1d ⊢ y = x → bday ⁡ y ⊆ bday ⁡ x ↔ bday ⁡ x ⊆ bday ⁡ x
41 eleq1 ⊢ y = x → y ∈ M ⁡ bday ⁡ x ↔ x ∈ M ⁡ bday ⁡ x
42 40 41 imbi12d ⊢ y = x → bday ⁡ y ⊆ bday ⁡ x → y ∈ M ⁡ bday ⁡ x ↔ bday ⁡ x ⊆ bday ⁡ x → x ∈ M ⁡ bday ⁡ x
43 38 42 rspc2v ⊢ bday ⁡ x ∈ a ∧ x ∈ No → ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b → bday ⁡ x ⊆ bday ⁡ x → x ∈ M ⁡ bday ⁡ x
44 33 34 43 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
45 30 44 mpi ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → x ∈ M ⁡ bday ⁡ x
46 29 45 sseldd ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No ∧ bday ⁡ x ∈ a → x ∈ M ⁡ a
47 46 ex ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No → bday ⁡ x ∈ a → x ∈ M ⁡ a
48 madebdaylemlrcut ⊢ ∀ b ∈ bday ⁡ x ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ x ∈ No → L ⁡ x | s R ⁡ x = x
49 20 a1i ⊢ x ∈ No → bday ⁡ x ∈ On
50 lltropt ⊢ x ∈ No → L ⁡ x ≪ s R ⁡ x
51 leftssold ⊢ x ∈ No → L ⁡ x ⊆ Old ⁡ bday ⁡ x
52 rightssold ⊢ 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 49 50 51 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 48 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 47 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 23 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 14 19 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 3 75 impbid ⊢ A ∈ On ∧ X ∈ No → X ∈ M ⁡ A ↔ bday ⁡ X ⊆ A