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

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ a = b → M ⁡ a = M ⁡ b
2 sseq2 ⊢ a = b → bday ⁡ x ⊆ a ↔ bday ⁡ x ⊆ b
3 1 2 raleqbidv ⊢ a = b → ∀ x ∈ M ⁡ a bday ⁡ x ⊆ a ↔ ∀ x ∈ M ⁡ b bday ⁡ x ⊆ b
4 fveq2 ⊢ x = y → bday ⁡ x = bday ⁡ y
5 4 sseq1d ⊢ x = y → bday ⁡ x ⊆ b ↔ bday ⁡ y ⊆ b
6 5 cbvralvw ⊢ ∀ x ∈ M ⁡ b bday ⁡ x ⊆ b ↔ ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b
7 3 6 bitrdi ⊢ a = b → ∀ x ∈ M ⁡ a bday ⁡ x ⊆ a ↔ ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b
8 fveq2 ⊢ a = A → M ⁡ a = M ⁡ A
9 sseq2 ⊢ a = A → bday ⁡ x ⊆ a ↔ bday ⁡ x ⊆ A
10 8 9 raleqbidv ⊢ a = A → ∀ x ∈ M ⁡ a bday ⁡ x ⊆ a ↔ ∀ x ∈ M ⁡ A bday ⁡ x ⊆ A
11 elmade2 ⊢ a ∈ On → x ∈ M ⁡ a ↔ ∃ l ∈ 𝒫 Old ⁡ a ∃ r ∈ 𝒫 Old ⁡ a l ≪ s r ∧ l | s r = x
12 11 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
13 pwuncl ⊢ l ∈ 𝒫 Old ⁡ a ∧ r ∈ 𝒫 Old ⁡ a → l ∪ r ∈ 𝒫 Old ⁡ a
14 13 elpwid ⊢ l ∈ 𝒫 Old ⁡ a ∧ r ∈ 𝒫 Old ⁡ a → l ∪ r ⊆ Old ⁡ a
15 simprr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → l ≪ s r
16 simpll ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → a ∈ On
17 dfss3 ⊢ l ∪ r ⊆ Old ⁡ a ↔ ∀ z ∈ l ∪ r z ∈ Old ⁡ a
18 fveq2 ⊢ y = z → bday ⁡ y = bday ⁡ z
19 18 sseq1d ⊢ y = z → bday ⁡ y ⊆ b ↔ bday ⁡ z ⊆ b
20 19 rspccv ⊢ ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → z ∈ M ⁡ b → bday ⁡ z ⊆ b
21 20 ralimi ⊢ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → ∀ b ∈ a z ∈ M ⁡ b → bday ⁡ z ⊆ b
22 rexim ⊢ ∀ b ∈ a z ∈ M ⁡ b → bday ⁡ z ⊆ b → ∃ b ∈ a z ∈ M ⁡ b → ∃ b ∈ a bday ⁡ z ⊆ b
23 21 22 syl ⊢ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → ∃ b ∈ a z ∈ M ⁡ b → ∃ b ∈ a bday ⁡ z ⊆ b
24 23 adantl ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → ∃ b ∈ a z ∈ M ⁡ b → ∃ b ∈ a bday ⁡ z ⊆ b
25 elold ⊢ a ∈ On → z ∈ Old ⁡ a ↔ ∃ b ∈ a z ∈ M ⁡ b
26 25 adantr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → z ∈ Old ⁡ a ↔ ∃ b ∈ a z ∈ M ⁡ b
27 bdayelon ⊢ bday ⁡ z ∈ On
28 onelssex ⊢ bday ⁡ z ∈ On ∧ a ∈ On → bday ⁡ z ∈ a ↔ ∃ b ∈ a bday ⁡ z ⊆ b
29 27 28 mpan ⊢ a ∈ On → bday ⁡ z ∈ a ↔ ∃ b ∈ a bday ⁡ z ⊆ b
30 29 adantr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → bday ⁡ z ∈ a ↔ ∃ b ∈ a bday ⁡ z ⊆ b
31 24 26 30 3imtr4d ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → z ∈ Old ⁡ a → bday ⁡ z ∈ a
32 31 ralimdv ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → ∀ z ∈ l ∪ r z ∈ Old ⁡ a → ∀ z ∈ l ∪ r bday ⁡ z ∈ a
33 17 32 syl5bi ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → l ∪ r ⊆ Old ⁡ a → ∀ z ∈ l ∪ r bday ⁡ z ∈ a
34 33 imp ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a → ∀ z ∈ l ∪ r bday ⁡ z ∈ a
35 34 adantrr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → ∀ z ∈ l ∪ r bday ⁡ z ∈ a
36 bdayfun ⊢ Fun ⁡ bday
37 ssltss1 ⊢ l ≪ s r → l ⊆ No
38 ssltss2 ⊢ l ≪ s r → r ⊆ No
39 37 38 unssd ⊢ l ≪ s r → l ∪ r ⊆ No
40 39 adantl ⊢ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → l ∪ r ⊆ No
41 40 adantl ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → l ∪ r ⊆ No
42 bdaydm ⊢ dom ⁡ bday = No
43 41 42 sseqtrrdi ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → l ∪ r ⊆ dom ⁡ bday
44 funimass4 ⊢ Fun ⁡ bday ∧ l ∪ r ⊆ dom ⁡ bday → bday l ∪ r ⊆ a ↔ ∀ z ∈ l ∪ r bday ⁡ z ∈ a
45 36 43 44 sylancr ⊢ 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
46 35 45 mpbird ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → bday l ∪ r ⊆ a
47 scutbdaybnd ⊢ l ≪ s r ∧ a ∈ On ∧ bday l ∪ r ⊆ a → bday ⁡ l | s r ⊆ a
48 15 16 46 47 syl3anc ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a ∧ l ≪ s r → bday ⁡ l | s r ⊆ a
49 fveq2 ⊢ l | s r = x → bday ⁡ l | s r = bday ⁡ x
50 49 sseq1d ⊢ l | s r = x → bday ⁡ l | s r ⊆ a ↔ bday ⁡ x ⊆ a
51 48 50 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
52 51 expr ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a → l ≪ s r → l | s r = x → bday ⁡ x ⊆ a
53 52 impd ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b ∧ l ∪ r ⊆ Old ⁡ a → l ≪ s r ∧ l | s r = x → bday ⁡ x ⊆ a
54 53 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
55 14 54 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
56 55 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
57 12 56 sylbid ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → x ∈ M ⁡ a → bday ⁡ x ⊆ a
58 57 ralrimiv ⊢ a ∈ On ∧ ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → ∀ x ∈ M ⁡ a bday ⁡ x ⊆ a
59 58 ex ⊢ a ∈ On → ∀ b ∈ a ∀ y ∈ M ⁡ b bday ⁡ y ⊆ b → ∀ x ∈ M ⁡ a bday ⁡ x ⊆ a
60 7 10 59 tfis3 ⊢ A ∈ On → ∀ x ∈ M ⁡ A bday ⁡ x ⊆ A
61 fveq2 ⊢ x = X → bday ⁡ x = bday ⁡ X
62 61 sseq1d ⊢ x = X → bday ⁡ x ⊆ A ↔ bday ⁡ X ⊆ A
63 62 rspccva ⊢ ∀ x ∈ M ⁡ A bday ⁡ x ⊆ A ∧ X ∈ M ⁡ A → bday ⁡ X ⊆ A
64 60 63 sylan ⊢ A ∈ On ∧ X ∈ M ⁡ A → bday ⁡ X ⊆ A