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

Theorem nosepne 31956
 Description: The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021.)
Assertion
Ref Expression
nosepne ((𝐴 No 𝐵 No 𝐴𝐵) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem nosepne
StepHypRef Expression
1 sltso 31952 . . . 4 <s Or No
2 sotrine 31784 . . . 4 (( <s Or No ∧ (𝐴 No 𝐵 No )) → (𝐴𝐵 ↔ (𝐴 <s 𝐵𝐵 <s 𝐴)))
31, 2mpan 706 . . 3 ((𝐴 No 𝐵 No ) → (𝐴𝐵 ↔ (𝐴 <s 𝐵𝐵 <s 𝐴)))
4 nosepnelem 31955 . . . . 5 ((𝐴 No 𝐵 No 𝐴 <s 𝐵) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
543expia 1286 . . . 4 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)})))
6 nosepnelem 31955 . . . . . . 7 ((𝐵 No 𝐴 No 𝐵 <s 𝐴) → (𝐵 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}) ≠ (𝐴 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}))
7 necom 2876 . . . . . . . . . . . 12 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ (𝐵𝑥) ≠ (𝐴𝑥))
87rabbii 3216 . . . . . . . . . . 11 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} = {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}
98inteqi 4511 . . . . . . . . . 10 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)} = {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}
109fveq2i 6232 . . . . . . . . 9 (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = (𝐴 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)})
119fveq2i 6232 . . . . . . . . 9 (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) = (𝐵 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)})
1210, 11neeq12i 2889 . . . . . . . 8 ((𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ↔ (𝐴 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}))
13 necom 2876 . . . . . . . 8 ((𝐴 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}) ↔ (𝐵 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}) ≠ (𝐴 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}))
1412, 13bitri 264 . . . . . . 7 ((𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ↔ (𝐵 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}) ≠ (𝐴 {𝑥 ∈ On ∣ (𝐵𝑥) ≠ (𝐴𝑥)}))
156, 14sylibr 224 . . . . . 6 ((𝐵 No 𝐴 No 𝐵 <s 𝐴) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
16153expia 1286 . . . . 5 ((𝐵 No 𝐴 No ) → (𝐵 <s 𝐴 → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)})))
1716ancoms 468 . . . 4 ((𝐴 No 𝐵 No ) → (𝐵 <s 𝐴 → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)})))
185, 17jaod 394 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 <s 𝐵𝐵 <s 𝐴) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)})))
193, 18sylbid 230 . 2 ((𝐴 No 𝐵 No ) → (𝐴𝐵 → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)})))
20193impia 1280 1 ((𝐴 No 𝐵 No 𝐴𝐵) → (𝐴 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}) ≠ (𝐵 {𝑥 ∈ On ∣ (𝐴𝑥) ≠ (𝐵𝑥)}))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   ∈ wcel 2030   ≠ wne 2823  {crab 2945  ∩ cint 4507   class class class wbr 4685   Or wor 5063  Oncon0 5761  ‘cfv 5926   No csur 31918
 Copyright terms: Public domain W3C validator