MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  slelss Structured version   Visualization version   GIF version
Theorem slelss 27639
Description: If two surreals ðī and ðĩ share a birthday, then ðī â‰Īs ðĩ if and only if the left set of ðī is a non-strict subset of the left set of ðĩ. (Contributed by Scott Fenton, 21-Mar-2025.)
Assertion
Ref Expression
slelss ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (ðī â‰Īs ðĩ ↔ ( L ‘ðī) ⊆ ( L ‘ðĩ)))
Proof of Theorem slelss
StepHypRef Expression
1 sltlpss 27638 . . 3 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (ðī <s ðĩ ↔ ( L ‘ðī) ⊊ ( L ‘ðĩ)))
2 fveq2 6890 . . . 4 (ðī = ðĩ → ( L ‘ðī) = ( L ‘ðĩ))
3 simpr 483 . . . . . . 7 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ( L ‘ðī) = ( L ‘ðĩ))
4 lruneq 27637 . . . . . . . . . 10 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (( L ‘ðī) ∊ ( R ‘ðī)) = (( L ‘ðĩ) ∊ ( R ‘ðĩ)))
54adantr 479 . . . . . . . . 9 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( L ‘ðī) ∊ ( R ‘ðī)) = (( L ‘ðĩ) ∊ ( R ‘ðĩ)))
65, 3difeq12d 4122 . . . . . . . 8 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ((( L ‘ðī) ∊ ( R ‘ðī)) ∖ ( L ‘ðī)) = ((( L ‘ðĩ) ∊ ( R ‘ðĩ)) ∖ ( L ‘ðĩ)))
7 difundir 4279 . . . . . . . . . 10 ((( L ‘ðī) ∊ ( R ‘ðī)) ∖ ( L ‘ðī)) = ((( L ‘ðī) ∖ ( L ‘ðī)) ∊ (( R ‘ðī) ∖ ( L ‘ðī)))
8 difid 4369 . . . . . . . . . . 11 (( L ‘ðī) ∖ ( L ‘ðī)) = ∅
98uneq1i 4158 . . . . . . . . . 10 ((( L ‘ðī) ∖ ( L ‘ðī)) ∊ (( R ‘ðī) ∖ ( L ‘ðī))) = (∅ ∊ (( R ‘ðī) ∖ ( L ‘ðī)))
10 0un 4391 . . . . . . . . . 10 (∅ ∊ (( R ‘ðī) ∖ ( L ‘ðī))) = (( R ‘ðī) ∖ ( L ‘ðī))
117, 9, 103eqtri 2762 . . . . . . . . 9 ((( L ‘ðī) ∊ ( R ‘ðī)) ∖ ( L ‘ðī)) = (( R ‘ðī) ∖ ( L ‘ðī))
12 incom 4200 . . . . . . . . . . 11 (( L ‘ðī) âˆĐ ( R ‘ðī)) = (( R ‘ðī) âˆĐ ( L ‘ðī))
13 lltropt 27604 . . . . . . . . . . . 12 ( L ‘ðī) <<s ( R ‘ðī)
14 ssltdisj 27559 . . . . . . . . . . . 12 (( L ‘ðī) <<s ( R ‘ðī) → (( L ‘ðī) âˆĐ ( R ‘ðī)) = ∅)
1513, 14mp1i 13 . . . . . . . . . . 11 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( L ‘ðī) âˆĐ ( R ‘ðī)) = ∅)
1612, 15eqtr3id 2784 . . . . . . . . . 10 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( R ‘ðī) âˆĐ ( L ‘ðī)) = ∅)
17 disjdif2 4478 . . . . . . . . . 10 ((( R ‘ðī) âˆĐ ( L ‘ðī)) = ∅ → (( R ‘ðī) ∖ ( L ‘ðī)) = ( R ‘ðī))
1816, 17syl 17 . . . . . . . . 9 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( R ‘ðī) ∖ ( L ‘ðī)) = ( R ‘ðī))
1911, 18eqtrid 2782 . . . . . . . 8 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ((( L ‘ðī) ∊ ( R ‘ðī)) ∖ ( L ‘ðī)) = ( R ‘ðī))
20 difundir 4279 . . . . . . . . . 10 ((( L ‘ðĩ) ∊ ( R ‘ðĩ)) ∖ ( L ‘ðĩ)) = ((( L ‘ðĩ) ∖ ( L ‘ðĩ)) ∊ (( R ‘ðĩ) ∖ ( L ‘ðĩ)))
21 difid 4369 . . . . . . . . . . 11 (( L ‘ðĩ) ∖ ( L ‘ðĩ)) = ∅
2221uneq1i 4158 . . . . . . . . . 10 ((( L ‘ðĩ) ∖ ( L ‘ðĩ)) ∊ (( R ‘ðĩ) ∖ ( L ‘ðĩ))) = (∅ ∊ (( R ‘ðĩ) ∖ ( L ‘ðĩ)))
23 0un 4391 . . . . . . . . . 10 (∅ ∊ (( R ‘ðĩ) ∖ ( L ‘ðĩ))) = (( R ‘ðĩ) ∖ ( L ‘ðĩ))
2420, 22, 233eqtri 2762 . . . . . . . . 9 ((( L ‘ðĩ) ∊ ( R ‘ðĩ)) ∖ ( L ‘ðĩ)) = (( R ‘ðĩ) ∖ ( L ‘ðĩ))
25 incom 4200 . . . . . . . . . . 11 (( L ‘ðĩ) âˆĐ ( R ‘ðĩ)) = (( R ‘ðĩ) âˆĐ ( L ‘ðĩ))
26 lltropt 27604 . . . . . . . . . . . 12 ( L ‘ðĩ) <<s ( R ‘ðĩ)
27 ssltdisj 27559 . . . . . . . . . . . 12 (( L ‘ðĩ) <<s ( R ‘ðĩ) → (( L ‘ðĩ) âˆĐ ( R ‘ðĩ)) = ∅)
2826, 27mp1i 13 . . . . . . . . . . 11 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( L ‘ðĩ) âˆĐ ( R ‘ðĩ)) = ∅)
2925, 28eqtr3id 2784 . . . . . . . . . 10 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( R ‘ðĩ) âˆĐ ( L ‘ðĩ)) = ∅)
30 disjdif2 4478 . . . . . . . . . 10 ((( R ‘ðĩ) âˆĐ ( L ‘ðĩ)) = ∅ → (( R ‘ðĩ) ∖ ( L ‘ðĩ)) = ( R ‘ðĩ))
3129, 30syl 17 . . . . . . . . 9 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( R ‘ðĩ) ∖ ( L ‘ðĩ)) = ( R ‘ðĩ))
3224, 31eqtrid 2782 . . . . . . . 8 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ((( L ‘ðĩ) ∊ ( R ‘ðĩ)) ∖ ( L ‘ðĩ)) = ( R ‘ðĩ))
336, 19, 323eqtr3d 2778 . . . . . . 7 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ( R ‘ðī) = ( R ‘ðĩ))
343, 33oveq12d 7429 . . . . . 6 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( L ‘ðī) |s ( R ‘ðī)) = (( L ‘ðĩ) |s ( R ‘ðĩ)))
35 simpl1 1189 . . . . . . 7 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ðī ∈ No )
36 lrcut 27634 . . . . . . 7 (ðī ∈ No → (( L ‘ðī) |s ( R ‘ðī)) = ðī)
3735, 36syl 17 . . . . . 6 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( L ‘ðī) |s ( R ‘ðī)) = ðī)
38 simpl2 1190 . . . . . . 7 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ðĩ ∈ No )
39 lrcut 27634 . . . . . . 7 (ðĩ ∈ No → (( L ‘ðĩ) |s ( R ‘ðĩ)) = ðĩ)
4038, 39syl 17 . . . . . 6 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → (( L ‘ðĩ) |s ( R ‘ðĩ)) = ðĩ)
4134, 37, 403eqtr3d 2778 . . . . 5 (((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) ∧ ( L ‘ðī) = ( L ‘ðĩ)) → ðī = ðĩ)
4241ex 411 . . . 4 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (( L ‘ðī) = ( L ‘ðĩ) → ðī = ðĩ))
432, 42impbid2 225 . . 3 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (ðī = ðĩ ↔ ( L ‘ðī) = ( L ‘ðĩ)))
441, 43orbi12d 915 . 2 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → ((ðī <s ðĩ âˆĻ ðī = ðĩ) ↔ (( L ‘ðī) ⊊ ( L ‘ðĩ) âˆĻ ( L ‘ðī) = ( L ‘ðĩ))))
45 sleloe 27493 . . 3 ((ðī ∈ No ∧ ðĩ ∈ No ) → (ðī â‰Īs ðĩ ↔ (ðī <s ðĩ âˆĻ ðī = ðĩ)))
46453adant3 1130 . 2 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (ðī â‰Īs ðĩ ↔ (ðī <s ðĩ âˆĻ ðī = ðĩ)))
47 sspss 4098 . . 3 (( L ‘ðī) ⊆ ( L ‘ðĩ) ↔ (( L ‘ðī) ⊊ ( L ‘ðĩ) âˆĻ ( L ‘ðī) = ( L ‘ðĩ)))
4847a1i 11 . 2 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (( L ‘ðī) ⊆ ( L ‘ðĩ) ↔ (( L ‘ðī) ⊊ ( L ‘ðĩ) âˆĻ ( L ‘ðī) = ( L ‘ðĩ))))
4944, 46, 483bitr4d 310 1 ((ðī ∈ No ∧ ðĩ ∈ No ∧ ( bday ‘ðī) = ( bday ‘ðĩ)) → (ðī â‰Īs ðĩ ↔ ( L ‘ðī) ⊆ ( L ‘ðĩ)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   âˆĻ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   ∖ cdif 3944   ∊ cun 3945   âˆĐ cin 3946   ⊆ wss 3947   ⊊ wpss 3948  âˆ…c0 4321   class class class wbr 5147  â€˜cfv 6542  (class class class)co 7411   No csur 27379   <s cslt 27380   bday cbday 27381   â‰Īs csle 27483   <<s csslt 27518   |s cscut 27520   L cleft 27577   R cright 27578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  df-2o 8469  df-no 27382  df-slt 27383  df-bday 27384  df-sle 27484  df-sslt 27519  df-scut 27521  df-made 27579  df-old 27580  df-left 27582  df-right 27583
This theorem is referenced by:  sltonold  27926
  Copyright terms: Public domain W3C validator