Metamath Proof Explorer

Theorem cutbdaylt

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 cutbdaylt ( ( 𝑋 ∈ 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 sltstr ⊢ ( ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ∧ { 𝑋 } ≠ ∅ ) → 𝐴 <<s 𝐵 )
6 1 2 4 5 syl3anc ⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s 𝐵 )
7 cutbday ⊢ ( 𝐴 <<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 cutsval ⊢ ( 𝐴 <<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 bdayon ⊢ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On
50 bdayon ⊢ ( 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 ‘ 𝑋 ) )