Metamath Proof Explorer


Theorem scutbdaybnd

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

Ref Expression
Assertion scutbdaybnd ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 )

Proof

Step Hyp Ref Expression
1 etasslt ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) → ∃ 𝑥 No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) )
2 simpl1 ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s 𝐵 )
3 scutbday ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
4 2 3 syl ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
5 bdayfn bday Fn No
6 ssrab2 { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No
7 sneq ( 𝑦 = 𝑥 → { 𝑦 } = { 𝑥 } )
8 7 breq2d ( 𝑦 = 𝑥 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑥 } ) )
9 7 breq1d ( 𝑦 = 𝑥 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑥 } <<s 𝐵 ) )
10 8 9 anbi12d ( 𝑦 = 𝑥 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) )
11 simprl ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → 𝑥 No )
12 simprr1 ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s { 𝑥 } )
13 simprr2 ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → { 𝑥 } <<s 𝐵 )
14 12 13 jca ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) )
15 10 11 14 elrabd ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
16 fnfvima ( ( bday Fn No ∧ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday 𝑥 ) ∈ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
17 5 6 15 16 mp3an12i ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday 𝑥 ) ∈ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
18 intss1 ( ( bday 𝑥 ) ∈ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday 𝑥 ) )
19 17 18 syl ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday 𝑥 ) )
20 4 19 eqsstrd ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday 𝑥 ) )
21 simprr3 ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday 𝑥 ) ⊆ 𝑂 )
22 20 21 sstrd ( ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 )
23 1 22 rexlimddv ( ( 𝐴 <<s 𝐵𝑂 ∈ On ∧ ( bday “ ( 𝐴𝐵 ) ) ⊆ 𝑂 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 )