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

Theorem nodenselem5 33077
 Description: Lemma for nodense 33081. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 33076 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
Assertion
Ref Expression
nodenselem5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴))
Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem nodenselem5
StepHypRef Expression
1 simpll 763 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 No )
2 simplr 765 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → 𝐵 No )
3 sltso 33066 . . . . . . . . . 10 <s Or No
4 sonr 5494 . . . . . . . . . 10 (( <s Or No 𝐴 No ) → ¬ 𝐴 <s 𝐴)
53, 4mpan 686 . . . . . . . . 9 (𝐴 No → ¬ 𝐴 <s 𝐴)
6 breq2 5066 . . . . . . . . . 10 (𝐴 = 𝐵 → (𝐴 <s 𝐴𝐴 <s 𝐵))
76notbid 319 . . . . . . . . 9 (𝐴 = 𝐵 → (¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵))
85, 7syl5ibcom 246 . . . . . . . 8 (𝐴 No → (𝐴 = 𝐵 → ¬ 𝐴 <s 𝐵))
98necon2ad 3035 . . . . . . 7 (𝐴 No → (𝐴 <s 𝐵𝐴𝐵))
109adantr 481 . . . . . 6 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵𝐴𝐵))
1110imp 407 . . . . 5 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → 𝐴𝐵)
1211adantrl 712 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴𝐵)
13 nosepdm 33073 . . . 4 ((𝐴 No 𝐵 No 𝐴𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ (dom 𝐴 ∪ dom 𝐵))
141, 2, 12, 13syl3anc 1365 . . 3 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ (dom 𝐴 ∪ dom 𝐵))
15 unidm 4131 . . . . 5 (( bday 𝐴) ∪ ( bday 𝐴)) = ( bday 𝐴)
16 simprl 767 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → ( bday 𝐴) = ( bday 𝐵))
1716uneq2d 4142 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (( bday 𝐴) ∪ ( bday 𝐴)) = (( bday 𝐴) ∪ ( bday 𝐵)))
1815, 17syl5reqr 2875 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (( bday 𝐴) ∪ ( bday 𝐵)) = ( bday 𝐴))
19 bdayval 33040 . . . . . 6 (𝐴 No → ( bday 𝐴) = dom 𝐴)
201, 19syl 17 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → ( bday 𝐴) = dom 𝐴)
21 bdayval 33040 . . . . . 6 (𝐵 No → ( bday 𝐵) = dom 𝐵)
222, 21syl 17 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → ( bday 𝐵) = dom 𝐵)
2320, 22uneq12d 4143 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (( bday 𝐴) ∪ ( bday 𝐵)) = (dom 𝐴 ∪ dom 𝐵))
2418, 23, 203eqtr3d 2868 . . 3 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (dom 𝐴 ∪ dom 𝐵) = dom 𝐴)
2514, 24eleqtrd 2919 . 2 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴)
2625, 20eleqtrrd 2920 1 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2106   ≠ wne 3020  {crab 3146   ∪ cun 3937  ∩ cint 4873   class class class wbr 5062   Or wor 5471  dom cdm 5553  Oncon0 6188  ‘cfv 6351   No csur 33032
 Copyright terms: Public domain W3C validator