Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  scutbdaylt Structured version   Visualization version   GIF version

Theorem scutbdaylt 32047
 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.)
Assertion
Ref Expression
scutbdaylt ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday 𝑋))

Proof of Theorem scutbdaylt
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2l 1107 . . . . 5 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝐴 <<s {𝑋})
2 simp2r 1108 . . . . 5 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → {𝑋} <<s 𝐵)
3 snnzg 4339 . . . . . 6 (𝑋 No → {𝑋} ≠ ∅)
433ad2ant1 1102 . . . . 5 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → {𝑋} ≠ ∅)
5 sslttr 32039 . . . . 5 ((𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵 ∧ {𝑋} ≠ ∅) → 𝐴 <<s 𝐵)
61, 2, 4, 5syl3anc 1366 . . . 4 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵)
7 scutbday 32038 . . . 4 (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
86, 7syl 17 . . 3 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
9 bdayfn 32014 . . . . 5 bday Fn No
10 ssrab2 3720 . . . . 5 {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
11 simp1 1081 . . . . . 6 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝑋 No )
12 simp2 1082 . . . . . 6 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵))
13 sneq 4220 . . . . . . . . 9 (𝑦 = 𝑋 → {𝑦} = {𝑋})
1413breq2d 4697 . . . . . . . 8 (𝑦 = 𝑋 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑋}))
1513breq1d 4695 . . . . . . . 8 (𝑦 = 𝑋 → ({𝑦} <<s 𝐵 ↔ {𝑋} <<s 𝐵))
1614, 15anbi12d 747 . . . . . . 7 (𝑦 = 𝑋 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)))
1716elrab 3396 . . . . . 6 (𝑋 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)))
1811, 12, 17sylanbrc 699 . . . . 5 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝑋 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})
19 fnfvima 6536 . . . . 5 (( bday Fn No ∧ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No 𝑋 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday 𝑋) ∈ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
209, 10, 18, 19mp3an12i 1468 . . . 4 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday 𝑋) ∈ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
21 intss1 4524 . . . 4 (( bday 𝑋) ∈ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday 𝑋))
2220, 21syl 17 . . 3 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday 𝑋))
238, 22eqsstrd 3672 . 2 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday 𝑋))
24 simprl 809 . . . . . . . . . . . 12 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → 𝐴 <<s {𝑋})
25 simprr 811 . . . . . . . . . . . 12 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → {𝑋} <<s 𝐵)
263adantr 480 . . . . . . . . . . . 12 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → {𝑋} ≠ ∅)
2724, 25, 26, 5syl3anc 1366 . . . . . . . . . . 11 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → 𝐴 <<s 𝐵)
2827, 7syl 17 . . . . . . . . . 10 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
2928eqeq1d 2653 . . . . . . . . 9 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋) ↔ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) = ( bday 𝑋)))
30 eqcom 2658 . . . . . . . . 9 ( ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) = ( bday 𝑋) ↔ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
3129, 30syl6bb 276 . . . . . . . 8 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋) ↔ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
3231biimpa 500 . . . . . . 7 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
3317biimpri 218 . . . . . . . 8 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → 𝑋 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})
3427adantr 480 . . . . . . . . 9 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → 𝐴 <<s 𝐵)
35 conway 32035 . . . . . . . . 9 (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
3634, 35syl 17 . . . . . . . 8 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → ∃!𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
37 fveq2 6229 . . . . . . . . . . 11 (𝑥 = 𝑋 → ( bday 𝑥) = ( bday 𝑋))
3837eqeq1d 2653 . . . . . . . . . 10 (𝑥 = 𝑋 → (( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
3938riota2 6673 . . . . . . . . 9 ((𝑋 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ∧ ∃!𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) → (( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) = 𝑋))
40 eqcom 2658 . . . . . . . . 9 ((𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) = 𝑋𝑋 = (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
4139, 40syl6bb 276 . . . . . . . 8 ((𝑋 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ∧ ∃!𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) → (( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ 𝑋 = (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))))
4233, 36, 41syl2an2r 893 . . . . . . 7 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → (( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ 𝑋 = (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))))
4332, 42mpbid 222 . . . . . 6 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → 𝑋 = (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
44 scutval 32036 . . . . . . 7 (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
4534, 44syl 17 . . . . . 6 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → (𝐴 |s 𝐵) = (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
4643, 45eqtr4d 2688 . . . . 5 (((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋)) → 𝑋 = (𝐴 |s 𝐵))
4746ex 449 . . . 4 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (( bday ‘(𝐴 |s 𝐵)) = ( bday 𝑋) → 𝑋 = (𝐴 |s 𝐵)))
4847necon3d 2844 . . 3 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (𝑋 ≠ (𝐴 |s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) ≠ ( bday 𝑋)))
49483impia 1280 . 2 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ≠ ( bday 𝑋))
50 bdayelon 32017 . . 3 ( bday ‘(𝐴 |s 𝐵)) ∈ On
51 bdayelon 32017 . . 3 ( bday 𝑋) ∈ On
52 onelpss 5802 . . 3 ((( bday ‘(𝐴 |s 𝐵)) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday 𝑋) ↔ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday 𝑋) ∧ ( bday ‘(𝐴 |s 𝐵)) ≠ ( bday 𝑋))))
5350, 51, 52mp2an 708 . 2 (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday 𝑋) ↔ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday 𝑋) ∧ ( bday ‘(𝐴 |s 𝐵)) ≠ ( bday 𝑋)))
5423, 49, 53sylanbrc 699 1 ((𝑋 No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday 𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∃!wreu 2943  {crab 2945   ⊆ wss 3607  ∅c0 3948  {csn 4210  ∩ cint 4507   class class class wbr 4685   “ cima 5146  Oncon0 5761   Fn wfn 5921  ‘cfv 5926  ℩crio 6650  (class class class)co 6690   No csur 31918   bday cbday 31920   <
 Copyright terms: Public domain W3C validator