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

Theorem nosepssdm 33197
Description: Given two non-equal surreals, their separator is less than or equal to the domain of one of them. Part of Lemma 2.1.1 of [Lipparini] p. 3. (Contributed by Scott Fenton, 6-Dec-2021.)
Assertion
Ref Expression
nosepssdm ((𝐴 No 𝐵 No 𝐴𝐵) → {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ⊆ dom 𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem nosepssdm
StepHypRef Expression
1 nosepne 33192 . . . 4 ((𝐴 No 𝐵 No 𝐴𝐵) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
21neneqd 3012 . . 3 ((𝐴 No 𝐵 No 𝐴𝐵) → ¬ (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
3 nodmord 33167 . . . . . . . . 9 (𝐴 No → Ord dom 𝐴)
433ad2ant1 1130 . . . . . . . 8 ((𝐴 No 𝐵 No 𝐴𝐵) → Ord dom 𝐴)
5 ordn2lp 6184 . . . . . . . 8 (Ord dom 𝐴 → ¬ (dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∧ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴))
64, 5syl 17 . . . . . . 7 ((𝐴 No 𝐵 No 𝐴𝐵) → ¬ (dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∧ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴))
7 imnan 403 . . . . . . 7 ((dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴) ↔ ¬ (dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∧ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴))
86, 7sylibr 237 . . . . . 6 ((𝐴 No 𝐵 No 𝐴𝐵) → (dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴))
98imp 410 . . . . 5 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴)
10 ndmfv 6673 . . . . 5 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐴 → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = ∅)
119, 10syl 17 . . . 4 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = ∅)
12 nosepeq 33196 . . . . . 6 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (𝐴‘dom 𝐴) = (𝐵‘dom 𝐴))
13 simpl1 1188 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → 𝐴 No )
1413, 3syl 17 . . . . . . . . . 10 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → Ord dom 𝐴)
15 ordirr 6182 . . . . . . . . . 10 (Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴)
16 ndmfv 6673 . . . . . . . . . 10 (¬ dom 𝐴 ∈ dom 𝐴 → (𝐴‘dom 𝐴) = ∅)
1714, 15, 163syl 18 . . . . . . . . 9 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (𝐴‘dom 𝐴) = ∅)
1817eqeq1d 2823 . . . . . . . 8 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ((𝐴‘dom 𝐴) = (𝐵‘dom 𝐴) ↔ ∅ = (𝐵‘dom 𝐴)))
19 eqcom 2828 . . . . . . . 8 (∅ = (𝐵‘dom 𝐴) ↔ (𝐵‘dom 𝐴) = ∅)
2018, 19syl6bb 290 . . . . . . 7 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ((𝐴‘dom 𝐴) = (𝐵‘dom 𝐴) ↔ (𝐵‘dom 𝐴) = ∅))
21 simpl2 1189 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → 𝐵 No )
22 nofun 33163 . . . . . . . . . . 11 (𝐵 No → Fun 𝐵)
2321, 22syl 17 . . . . . . . . . 10 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → Fun 𝐵)
24 nosgnn0 33172 . . . . . . . . . . 11 ¬ ∅ ∈ {1o, 2o}
25 norn 33165 . . . . . . . . . . . . 13 (𝐵 No → ran 𝐵 ⊆ {1o, 2o})
2621, 25syl 17 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ran 𝐵 ⊆ {1o, 2o})
2726sseld 3942 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (∅ ∈ ran 𝐵 → ∅ ∈ {1o, 2o}))
2824, 27mtoi 202 . . . . . . . . . 10 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ¬ ∅ ∈ ran 𝐵)
29 funeldmb 33013 . . . . . . . . . 10 ((Fun 𝐵 ∧ ¬ ∅ ∈ ran 𝐵) → (dom 𝐴 ∈ dom 𝐵 ↔ (𝐵‘dom 𝐴) ≠ ∅))
3023, 28, 29syl2anc 587 . . . . . . . . 9 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (dom 𝐴 ∈ dom 𝐵 ↔ (𝐵‘dom 𝐴) ≠ ∅))
3130necon2bbid 3050 . . . . . . . 8 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ((𝐵‘dom 𝐴) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐵))
32 nodmord 33167 . . . . . . . . . . . 12 (𝐵 No → Ord dom 𝐵)
33323ad2ant2 1131 . . . . . . . . . . 11 ((𝐴 No 𝐵 No 𝐴𝐵) → Ord dom 𝐵)
34 ordtr1 6207 . . . . . . . . . . 11 (Ord dom 𝐵 → ((dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∧ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵) → dom 𝐴 ∈ dom 𝐵))
3533, 34syl 17 . . . . . . . . . 10 ((𝐴 No 𝐵 No 𝐴𝐵) → ((dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∧ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵) → dom 𝐴 ∈ dom 𝐵))
3635expdimp 456 . . . . . . . . 9 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ( {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵 → dom 𝐴 ∈ dom 𝐵))
3736con3d 155 . . . . . . . 8 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (¬ dom 𝐴 ∈ dom 𝐵 → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵))
3831, 37sylbid 243 . . . . . . 7 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ((𝐵‘dom 𝐴) = ∅ → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵))
3920, 38sylbid 243 . . . . . 6 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ((𝐴‘dom 𝐴) = (𝐵‘dom 𝐴) → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵))
4012, 39mpd 15 . . . . 5 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → ¬ {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵)
41 ndmfv 6673 . . . . 5 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ dom 𝐵 → (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = ∅)
4240, 41syl 17 . . . 4 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = ∅)
4311, 42eqtr4d 2859 . . 3 (((𝐴 No 𝐵 No 𝐴𝐵) ∧ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
442, 43mtand 815 . 2 ((𝐴 No 𝐵 No 𝐴𝐵) → ¬ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)})
45 nosepon 33179 . . 3 ((𝐴 No 𝐵 No 𝐴𝐵) → {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ On)
46 nodmon 33164 . . . 4 (𝐴 No → dom 𝐴 ∈ On)
47463ad2ant1 1130 . . 3 ((𝐴 No 𝐵 No 𝐴𝐵) → dom 𝐴 ∈ On)
48 ontri1 6198 . . 3 (( {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ∈ On ∧ dom 𝐴 ∈ On) → ( {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ⊆ dom 𝐴 ↔ ¬ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
4945, 47, 48syl2anc 587 . 2 ((𝐴 No 𝐵 No 𝐴𝐵) → ( {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ⊆ dom 𝐴 ↔ ¬ dom 𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
5044, 49mpbird 260 1 ((𝐴 No 𝐵 No 𝐴𝐵) → {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} ⊆ dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  wne 3007  {crab 3130  wss 3910  c0 4266  {cpr 4542   cint 4849  dom cdm 5528  ran crn 5529  Ord word 6163  Oncon0 6164  Fun wfun 6322  cfv 6328  1oc1o 8070  2oc2o 8071   No csur 33154
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-ord 6167  df-on 6168  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-1o 8077  df-2o 8078  df-no 33157  df-slt 33158
This theorem is referenced by:  nosupbnd2lem1  33222  noetalem3  33226
  Copyright terms: Public domain W3C validator