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 biimtrid ⊢ 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