Metamath Proof Explorer

Theorem cutbdaybnd2

Description: An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021)

Ref Expression
Assertion cutbdaybnd2 ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 etaslts2 ⊢ ( 𝐴 <<s 𝐵 → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
2 cutbday ⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
3 2 adantr ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
4 bdayfn ⊢ bday Fn No
5 ssrab2 ⊢ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No
6 simprl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → 𝑥 ∈ No )
7 simprr1 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → 𝐴 <<s { 𝑥 } )
8 simprr2 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → { 𝑥 } <<s 𝐵 )
9 7 8 jca ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) )
10 sneq ⊢ ( 𝑦 = 𝑥 → { 𝑦 } = { 𝑥 } )
11 10 breq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑥 } ) )
12 10 breq1d ⊢ ( 𝑦 = 𝑥 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑥 } <<s 𝐵 ) )
13 11 12 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) )
14 13 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) )
15 6 9 14 sylanbrc ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
16 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No ∧ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
17 4 5 15 16 mp3an12i ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
18 intss1 ⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) )
19 17 18 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) )
20 3 19 eqsstrd ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑥 ) )
21 simprr3 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
22 20 21 sstrd ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
23 22 rexlimdvaa ⊢ ( 𝐴 <<s 𝐵 → ( ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
24 1 23 mpd ⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )