MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  negsproplem2 Structured version   Visualization version   GIF version

Theorem negsproplem2 27385
Description: Lemma for surreal negation. Show that the cut that defines negation is legitimate. (Contributed by Scott Fenton, 2-Feb-2025.)
Hypotheses
Ref Expression
negsproplem.1 (𝜑 → ∀𝑥 No 𝑦 No ((( bday 𝑥) ∪ ( bday 𝑦)) ∈ (( bday 𝐴) ∪ ( bday 𝐵)) → (( -us𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us𝑦) <s ( -us𝑥)))))
negsproplem2.1 (𝜑𝐴 No )
Assertion
Ref Expression
negsproplem2 (𝜑 → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem negsproplem2
Dummy variables 𝑎 𝑏 𝑥𝐿 𝑥𝑅 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 negsfn 27380 . . . 4 -us Fn No
2 fnfun 6622 . . . 4 ( -us Fn No → Fun -us )
31, 2ax-mp 5 . . 3 Fun -us
4 fvex 6875 . . . 4 ( R ‘𝐴) ∈ V
54funimaex 6609 . . 3 (Fun -us → ( -us “ ( R ‘𝐴)) ∈ V)
63, 5mp1i 13 . 2 (𝜑 → ( -us “ ( R ‘𝐴)) ∈ V)
7 fvex 6875 . . . 4 ( L ‘𝐴) ∈ V
87funimaex 6609 . . 3 (Fun -us → ( -us “ ( L ‘𝐴)) ∈ V)
93, 8mp1i 13 . 2 (𝜑 → ( -us “ ( L ‘𝐴)) ∈ V)
10 rightssold 27267 . . . 4 ( R ‘𝐴) ⊆ ( O ‘( bday 𝐴))
11 imass2 6074 . . . 4 (( R ‘𝐴) ⊆ ( O ‘( bday 𝐴)) → ( -us “ ( R ‘𝐴)) ⊆ ( -us “ ( O ‘( bday 𝐴))))
1210, 11ax-mp 5 . . 3 ( -us “ ( R ‘𝐴)) ⊆ ( -us “ ( O ‘( bday 𝐴)))
13 negsproplem.1 . . . . . . . 8 (𝜑 → ∀𝑥 No 𝑦 No ((( bday 𝑥) ∪ ( bday 𝑦)) ∈ (( bday 𝐴) ∪ ( bday 𝐵)) → (( -us𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us𝑦) <s ( -us𝑥)))))
1413adantr 481 . . . . . . 7 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → ∀𝑥 No 𝑦 No ((( bday 𝑥) ∪ ( bday 𝑦)) ∈ (( bday 𝐴) ∪ ( bday 𝐵)) → (( -us𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us𝑦) <s ( -us𝑥)))))
15 oldssno 27249 . . . . . . . . 9 ( O ‘( bday 𝐴)) ⊆ No
1615sseli 3958 . . . . . . . 8 (𝑎 ∈ ( O ‘( bday 𝐴)) → 𝑎 No )
1716adantl 482 . . . . . . 7 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → 𝑎 No )
18 0sno 27223 . . . . . . . 8 0s No
1918a1i 11 . . . . . . 7 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → 0s No )
20 bday0s 27225 . . . . . . . . . 10 ( bday ‘ 0s ) = ∅
2120uneq2i 4140 . . . . . . . . 9 (( bday 𝑎) ∪ ( bday ‘ 0s )) = (( bday 𝑎) ∪ ∅)
22 un0 4370 . . . . . . . . 9 (( bday 𝑎) ∪ ∅) = ( bday 𝑎)
2321, 22eqtri 2759 . . . . . . . 8 (( bday 𝑎) ∪ ( bday ‘ 0s )) = ( bday 𝑎)
24 oldbdayim 27276 . . . . . . . . . 10 (𝑎 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑎) ∈ ( bday 𝐴))
2524adantl 482 . . . . . . . . 9 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → ( bday 𝑎) ∈ ( bday 𝐴))
26 elun1 4156 . . . . . . . . 9 (( bday 𝑎) ∈ ( bday 𝐴) → ( bday 𝑎) ∈ (( bday 𝐴) ∪ ( bday 𝐵)))
2725, 26syl 17 . . . . . . . 8 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → ( bday 𝑎) ∈ (( bday 𝐴) ∪ ( bday 𝐵)))
2823, 27eqeltrid 2836 . . . . . . 7 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → (( bday 𝑎) ∪ ( bday ‘ 0s )) ∈ (( bday 𝐴) ∪ ( bday 𝐵)))
2914, 17, 19, 28negsproplem1 27384 . . . . . 6 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → (( -us𝑎) ∈ No ∧ (𝑎 <s 0s → ( -us ‘ 0s ) <s ( -us𝑎))))
3029simpld 495 . . . . 5 ((𝜑𝑎 ∈ ( O ‘( bday 𝐴))) → ( -us𝑎) ∈ No )
3130ralrimiva 3145 . . . 4 (𝜑 → ∀𝑎 ∈ ( O ‘( bday 𝐴))( -us𝑎) ∈ No )
321fndmi 6626 . . . . . 6 dom -us = No
3315, 32sseqtrri 3999 . . . . 5 ( O ‘( bday 𝐴)) ⊆ dom -us
34 funimass4 6927 . . . . 5 ((Fun -us ∧ ( O ‘( bday 𝐴)) ⊆ dom -us ) → (( -us “ ( O ‘( bday 𝐴))) ⊆ No ↔ ∀𝑎 ∈ ( O ‘( bday 𝐴))( -us𝑎) ∈ No ))
353, 33, 34mp2an 690 . . . 4 (( -us “ ( O ‘( bday 𝐴))) ⊆ No ↔ ∀𝑎 ∈ ( O ‘( bday 𝐴))( -us𝑎) ∈ No )
3631, 35sylibr 233 . . 3 (𝜑 → ( -us “ ( O ‘( bday 𝐴))) ⊆ No )
3712, 36sstrid 3973 . 2 (𝜑 → ( -us “ ( R ‘𝐴)) ⊆ No )
38 leftssold 27266 . . . 4 ( L ‘𝐴) ⊆ ( O ‘( bday 𝐴))
39 imass2 6074 . . . 4 (( L ‘𝐴) ⊆ ( O ‘( bday 𝐴)) → ( -us “ ( L ‘𝐴)) ⊆ ( -us “ ( O ‘( bday 𝐴))))
4038, 39ax-mp 5 . . 3 ( -us “ ( L ‘𝐴)) ⊆ ( -us “ ( O ‘( bday 𝐴)))
4140, 36sstrid 3973 . 2 (𝜑 → ( -us “ ( L ‘𝐴)) ⊆ No )
42 rightssno 27269 . . . . . . 7 ( R ‘𝐴) ⊆ No
43 fvelimab 6934 . . . . . . 7 (( -us Fn No ∧ ( R ‘𝐴) ⊆ No ) → (𝑎 ∈ ( -us “ ( R ‘𝐴)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)( -us𝑥𝑅) = 𝑎))
441, 42, 43mp2an 690 . . . . . 6 (𝑎 ∈ ( -us “ ( R ‘𝐴)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)( -us𝑥𝑅) = 𝑎)
45 leftssno 27268 . . . . . . 7 ( L ‘𝐴) ⊆ No
46 fvelimab 6934 . . . . . . 7 (( -us Fn No ∧ ( L ‘𝐴) ⊆ No ) → (𝑏 ∈ ( -us “ ( L ‘𝐴)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us𝑥𝐿) = 𝑏))
471, 45, 46mp2an 690 . . . . . 6 (𝑏 ∈ ( -us “ ( L ‘𝐴)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us𝑥𝐿) = 𝑏)
4844, 47anbi12i 627 . . . . 5 ((𝑎 ∈ ( -us “ ( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L ‘𝐴))) ↔ (∃𝑥𝑅 ∈ ( R ‘𝐴)( -us𝑥𝑅) = 𝑎 ∧ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us𝑥𝐿) = 𝑏))
49 reeanv 3225 . . . . 5 (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us𝑥𝑅) = 𝑎 ∧ ( -us𝑥𝐿) = 𝑏) ↔ (∃𝑥𝑅 ∈ ( R ‘𝐴)( -us𝑥𝑅) = 𝑎 ∧ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us𝑥𝐿) = 𝑏))
5048, 49bitr4i 277 . . . 4 ((𝑎 ∈ ( -us “ ( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L ‘𝐴))) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us𝑥𝑅) = 𝑎 ∧ ( -us𝑥𝐿) = 𝑏))
51 lltropt 27260 . . . . . . . . 9 ( L ‘𝐴) <<s ( R ‘𝐴)
5251a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( L ‘𝐴) <<s ( R ‘𝐴))
53 simprr 771 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ ( L ‘𝐴))
54 simprl 769 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ ( R ‘𝐴))
5552, 53, 54ssltsepcd 27191 . . . . . . 7 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 <s 𝑥𝑅)
5613adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ∀𝑥 No 𝑦 No ((( bday 𝑥) ∪ ( bday 𝑦)) ∈ (( bday 𝐴) ∪ ( bday 𝐵)) → (( -us𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us𝑦) <s ( -us𝑥)))))
5745sseli 3958 . . . . . . . . . 10 (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 No )
5857ad2antll 727 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 No )
5942sseli 3958 . . . . . . . . . . 11 (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 No )
6059adantr 481 . . . . . . . . . 10 ((𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴)) → 𝑥𝑅 No )
6160adantl 482 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 No )
6238sseli 3958 . . . . . . . . . . . . 13 (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 ∈ ( O ‘( bday 𝐴)))
6362ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ ( O ‘( bday 𝐴)))
64 oldbdayim 27276 . . . . . . . . . . . 12 (𝑥𝐿 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑥𝐿) ∈ ( bday 𝐴))
6563, 64syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( bday 𝑥𝐿) ∈ ( bday 𝐴))
6610a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ( R ‘𝐴) ⊆ ( O ‘( bday 𝐴)))
6766sselda 3962 . . . . . . . . . . . . 13 ((𝜑𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ ( O ‘( bday 𝐴)))
6867adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ ( O ‘( bday 𝐴)))
69 oldbdayim 27276 . . . . . . . . . . . 12 (𝑥𝑅 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑥𝑅) ∈ ( bday 𝐴))
7068, 69syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( bday 𝑥𝑅) ∈ ( bday 𝐴))
71 bdayelon 27174 . . . . . . . . . . . 12 ( bday 𝑥𝐿) ∈ On
72 bdayelon 27174 . . . . . . . . . . . 12 ( bday 𝑥𝑅) ∈ On
73 bdayelon 27174 . . . . . . . . . . . 12 ( bday 𝐴) ∈ On
74 onunel 6442 . . . . . . . . . . . 12 ((( bday 𝑥𝐿) ∈ On ∧ ( bday 𝑥𝑅) ∈ On ∧ ( bday 𝐴) ∈ On) → ((( bday 𝑥𝐿) ∪ ( bday 𝑥𝑅)) ∈ ( bday 𝐴) ↔ (( bday 𝑥𝐿) ∈ ( bday 𝐴) ∧ ( bday 𝑥𝑅) ∈ ( bday 𝐴))))
7571, 72, 73, 74mp3an 1461 . . . . . . . . . . 11 ((( bday 𝑥𝐿) ∪ ( bday 𝑥𝑅)) ∈ ( bday 𝐴) ↔ (( bday 𝑥𝐿) ∈ ( bday 𝐴) ∧ ( bday 𝑥𝑅) ∈ ( bday 𝐴)))
7665, 70, 75sylanbrc 583 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( bday 𝑥𝐿) ∪ ( bday 𝑥𝑅)) ∈ ( bday 𝐴))
77 elun1 4156 . . . . . . . . . 10 ((( bday 𝑥𝐿) ∪ ( bday 𝑥𝑅)) ∈ ( bday 𝐴) → (( bday 𝑥𝐿) ∪ ( bday 𝑥𝑅)) ∈ (( bday 𝐴) ∪ ( bday 𝐵)))
7876, 77syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( bday 𝑥𝐿) ∪ ( bday 𝑥𝑅)) ∈ (( bday 𝐴) ∪ ( bday 𝐵)))
7956, 58, 61, 78negsproplem1 27384 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( -us𝑥𝐿) ∈ No ∧ (𝑥𝐿 <s 𝑥𝑅 → ( -us𝑥𝑅) <s ( -us𝑥𝐿))))
8079simprd 496 . . . . . . 7 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (𝑥𝐿 <s 𝑥𝑅 → ( -us𝑥𝑅) <s ( -us𝑥𝐿)))
8155, 80mpd 15 . . . . . 6 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( -us𝑥𝑅) <s ( -us𝑥𝐿))
82 breq12 5130 . . . . . 6 ((( -us𝑥𝑅) = 𝑎 ∧ ( -us𝑥𝐿) = 𝑏) → (( -us𝑥𝑅) <s ( -us𝑥𝐿) ↔ 𝑎 <s 𝑏))
8381, 82syl5ibcom 244 . . . . 5 ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ((( -us𝑥𝑅) = 𝑎 ∧ ( -us𝑥𝐿) = 𝑏) → 𝑎 <s 𝑏))
8483rexlimdvva 3210 . . . 4 (𝜑 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us𝑥𝑅) = 𝑎 ∧ ( -us𝑥𝐿) = 𝑏) → 𝑎 <s 𝑏))
8550, 84biimtrid 241 . . 3 (𝜑 → ((𝑎 ∈ ( -us “ ( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L ‘𝐴))) → 𝑎 <s 𝑏))
86853impib 1116 . 2 ((𝜑𝑎 ∈ ( -us “ ( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L ‘𝐴))) → 𝑎 <s 𝑏)
876, 9, 37, 41, 86ssltd 27189 1 (𝜑 → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3060  wrex 3069  Vcvv 3459  cun 3926  wss 3928  c0 4302   class class class wbr 5125  dom cdm 5653  cima 5656  Oncon0 6337  Fun wfun 6510   Fn wfn 6511  cfv 6516   No csur 27040   <s cslt 27041   bday cbday 27042   <<s csslt 27178   0s c0s 27219   O cold 27231   L cleft 27233   R cright 27234   -us cnegs 27376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-pss 3947  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4886  df-int 4928  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-tr 5243  df-id 5551  df-eprel 5557  df-po 5565  df-so 5566  df-fr 5608  df-se 5609  df-we 5610  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-pred 6273  df-ord 6340  df-on 6341  df-suc 6343  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-2nd 7942  df-frecs 8232  df-wrecs 8263  df-recs 8337  df-1o 8432  df-2o 8433  df-no 27043  df-slt 27044  df-bday 27045  df-sslt 27179  df-scut 27181  df-0s 27221  df-made 27235  df-old 27236  df-left 27238  df-right 27239  df-norec 27308  df-negs 27378
This theorem is referenced by:  negsproplem3  27386
  Copyright terms: Public domain W3C validator