Metamath Proof Explorer


Theorem scutbdaylt

Description: If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021)

Ref Expression
Assertion scutbdaylt ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday 𝑋 ) )

Proof

Step Hyp Ref Expression
1 simp2l ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s { 𝑋 } )
2 simp2r ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → { 𝑋 } <<s 𝐵 )
3 snnzg ( 𝑋 No → { 𝑋 } ≠ ∅ )
4 3 3ad2ant1 ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → { 𝑋 } ≠ ∅ )
5 sslttr ( ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ∧ { 𝑋 } ≠ ∅ ) → 𝐴 <<s 𝐵 )
6 1 2 4 5 syl3anc ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s 𝐵 )
7 scutbday ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
8 6 7 syl ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
9 bdayfn bday Fn No
10 ssrab2 { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No
11 simp1 ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝑋 No )
12 simp2 ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) )
13 sneq ( 𝑦 = 𝑋 → { 𝑦 } = { 𝑋 } )
14 13 breq2d ( 𝑦 = 𝑋 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑋 } ) )
15 13 breq1d ( 𝑦 = 𝑋 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑋 } <<s 𝐵 ) )
16 14 15 anbi12d ( 𝑦 = 𝑋 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) )
17 16 elrab ( 𝑋 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) )
18 11 12 17 sylanbrc ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝑋 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
19 fnfvima ( ( bday Fn No ∧ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No 𝑋 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday 𝑋 ) ∈ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
20 9 10 18 19 mp3an12i ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday 𝑋 ) ∈ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
21 intss1 ( ( bday 𝑋 ) ∈ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday 𝑋 ) )
22 20 21 syl ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday 𝑋 ) )
23 8 22 eqsstrd ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday 𝑋 ) )
24 simprl ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → 𝐴 <<s { 𝑋 } )
25 simprr ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → { 𝑋 } <<s 𝐵 )
26 3 adantr ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → { 𝑋 } ≠ ∅ )
27 24 25 26 5 syl3anc ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → 𝐴 <<s 𝐵 )
28 27 7 syl ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
29 28 eqeq1d ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ↔ ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) = ( bday 𝑋 ) ) )
30 eqcom ( ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) = ( bday 𝑋 ) ↔ ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
31 29 30 bitrdi ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ↔ ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
32 31 biimpa ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
33 17 biimpri ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → 𝑋 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
34 27 adantr ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → 𝐴 <<s 𝐵 )
35 conway ( 𝐴 <<s 𝐵 → ∃! 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
36 34 35 syl ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → ∃! 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
37 fveqeq2 ( 𝑥 = 𝑋 → ( ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
38 37 riota2 ( ( 𝑋 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∧ ∃! 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) → ( ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) = 𝑋 ) )
39 eqcom ( ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) = 𝑋𝑋 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
40 38 39 bitrdi ( ( 𝑋 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∧ ∃! 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) → ( ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ 𝑋 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) )
41 33 36 40 syl2an2r ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → ( ( bday 𝑋 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ 𝑋 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) )
42 32 41 mpbid ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → 𝑋 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
43 scutval ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
44 34 43 syl ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
45 42 44 eqtr4d ( ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
46 45 ex ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday 𝑋 ) → 𝑋 = ( 𝐴 |s 𝐵 ) ) )
47 46 necon3d ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( 𝑋 ≠ ( 𝐴 |s 𝐵 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday 𝑋 ) ) )
48 47 3impia ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday 𝑋 ) )
49 bdayelon ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On
50 bdayelon ( bday 𝑋 ) ∈ On
51 onelpss ( ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On ∧ ( bday 𝑋 ) ∈ On ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday 𝑋 ) ↔ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday 𝑋 ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday 𝑋 ) ) ) )
52 49 50 51 mp2an ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday 𝑋 ) ↔ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday 𝑋 ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday 𝑋 ) ) )
53 23 48 52 sylanbrc ( ( 𝑋 No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday 𝑋 ) )