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

Theorem nodenselem5 31084
 Description: Lemma for nodense 31088. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 31083 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
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sltirr 31069 . . . . . . . . 9 (𝐴 No → ¬ 𝐴 <s 𝐴)
2 breq2 4587 . . . . . . . . . 10 (𝐴 = 𝐵 → (𝐴 <s 𝐴𝐴 <s 𝐵))
32notbid 307 . . . . . . . . 9 (𝐴 = 𝐵 → (¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵))
41, 3syl5ibcom 234 . . . . . . . 8 (𝐴 No → (𝐴 = 𝐵 → ¬ 𝐴 <s 𝐵))
54con2d 128 . . . . . . 7 (𝐴 No → (𝐴 <s 𝐵 → ¬ 𝐴 = 𝐵))
65imp 444 . . . . . 6 ((𝐴 No 𝐴 <s 𝐵) → ¬ 𝐴 = 𝐵)
76ad2ant2rl 781 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (dom 𝐴 = dom 𝐵𝐴 <s 𝐵)) → ¬ 𝐴 = 𝐵)
8 nofun 31046 . . . . . . . . 9 (𝐴 No → Fun 𝐴)
9 nofun 31046 . . . . . . . . 9 (𝐵 No → Fun 𝐵)
10 eqfunfv 6224 . . . . . . . . 9 ((Fun 𝐴 ∧ Fun 𝐵) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))))
118, 9, 10syl2an 493 . . . . . . . 8 ((𝐴 No 𝐵 No ) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))))
1211notbid 307 . . . . . . 7 ((𝐴 No 𝐵 No ) → (¬ 𝐴 = 𝐵 ↔ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))))
1312adantr 480 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (dom 𝐴 = dom 𝐵𝐴 <s 𝐵)) → (¬ 𝐴 = 𝐵 ↔ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))))
14 imnan 437 . . . . . . . . . . . 12 ((dom 𝐴 = dom 𝐵 → ¬ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)) ↔ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)))
1514biimpri 217 . . . . . . . . . . 11 (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)) → (dom 𝐴 = dom 𝐵 → ¬ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)))
1615impcom 445 . . . . . . . . . 10 ((dom 𝐴 = dom 𝐵 ∧ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))) → ¬ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))
17 df-ne 2782 . . . . . . . . . . . . 13 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ (𝐴𝑥) = (𝐵𝑥))
1817rexbii 3023 . . . . . . . . . . . 12 (∃𝑥 ∈ dom 𝐴(𝐴𝑥) ≠ (𝐵𝑥) ↔ ∃𝑥 ∈ dom 𝐴 ¬ (𝐴𝑥) = (𝐵𝑥))
19 rexnal 2978 . . . . . . . . . . . 12 (∃𝑥 ∈ dom 𝐴 ¬ (𝐴𝑥) = (𝐵𝑥) ↔ ¬ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))
2018, 19bitri 263 . . . . . . . . . . 11 (∃𝑥 ∈ dom 𝐴(𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))
21 nodenselem4 31083 . . . . . . . . . . . . . . 15 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
22 eloni 5650 . . . . . . . . . . . . . . 15 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On → Ord {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
2321, 22syl 17 . . . . . . . . . . . . . 14 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → Ord {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
2423adantr 480 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥))) → Ord {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
25 nodmord 31050 . . . . . . . . . . . . . 14 (𝐴 No → Ord dom 𝐴)
2625ad3antrrr 762 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥))) → Ord dom 𝐴)
27 nodmon 31047 . . . . . . . . . . . . . . . . . . 19 (𝐴 No → dom 𝐴 ∈ On)
28 onelon 5665 . . . . . . . . . . . . . . . . . . 19 ((dom 𝐴 ∈ On ∧ 𝑥 ∈ dom 𝐴) → 𝑥 ∈ On)
2927, 28sylan 487 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑥 ∈ dom 𝐴) → 𝑥 ∈ On)
3029ex 449 . . . . . . . . . . . . . . . . 17 (𝐴 No → (𝑥 ∈ dom 𝐴𝑥 ∈ On))
3130ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → (𝑥 ∈ dom 𝐴𝑥 ∈ On))
3231anim1d 586 . . . . . . . . . . . . . . 15 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → ((𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥))))
3332imp 444 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥))) → (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)))
34 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐴𝑎) = (𝐴𝑥))
35 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐵𝑎) = (𝐵𝑥))
3634, 35neeq12d 2843 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑥) ≠ (𝐵𝑥)))
3736intminss 4438 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
3833, 37syl 17 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥))) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
39 simprl 790 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥))) → 𝑥 ∈ dom 𝐴)
40 ordtr2 5685 . . . . . . . . . . . . . 14 ((Ord {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∧ Ord dom 𝐴) → (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥𝑥 ∈ dom 𝐴) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
4140imp 444 . . . . . . . . . . . . 13 (((Ord {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∧ Ord dom 𝐴) ∧ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥𝑥 ∈ dom 𝐴)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴)
4224, 26, 38, 39, 41syl22anc 1319 . . . . . . . . . . . 12 ((((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴𝑥) ≠ (𝐵𝑥))) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴)
4342rexlimdvaa 3014 . . . . . . . . . . 11 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → (∃𝑥 ∈ dom 𝐴(𝐴𝑥) ≠ (𝐵𝑥) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
4420, 43syl5bir 232 . . . . . . . . . 10 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → (¬ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
4516, 44syl5 33 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → ((dom 𝐴 = dom 𝐵 ∧ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥))) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
4645exp4b 630 . . . . . . . 8 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 → (dom 𝐴 = dom 𝐵 → (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))))
4746com23 84 . . . . . . 7 ((𝐴 No 𝐵 No ) → (dom 𝐴 = dom 𝐵 → (𝐴 <s 𝐵 → (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))))
4847imp32 448 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (dom 𝐴 = dom 𝐵𝐴 <s 𝐵)) → (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴𝑥) = (𝐵𝑥)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
4913, 48sylbid 229 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (dom 𝐴 = dom 𝐵𝐴 <s 𝐵)) → (¬ 𝐴 = 𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
507, 49mpd 15 . . . 4 (((𝐴 No 𝐵 No ) ∧ (dom 𝐴 = dom 𝐵𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴)
5150ex 449 . . 3 ((𝐴 No 𝐵 No ) → ((dom 𝐴 = dom 𝐵𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
52 bdayval 31045 . . . . 5 (𝐴 No → ( bday 𝐴) = dom 𝐴)
53 bdayval 31045 . . . . 5 (𝐵 No → ( bday 𝐵) = dom 𝐵)
5452, 53eqeqan12d 2626 . . . 4 ((𝐴 No 𝐵 No ) → (( bday 𝐴) = ( bday 𝐵) ↔ dom 𝐴 = dom 𝐵))
5554anbi1d 737 . . 3 ((𝐴 No 𝐵 No ) → ((( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵) ↔ (dom 𝐴 = dom 𝐵𝐴 <s 𝐵)))
5652eleq2d 2673 . . . 4 (𝐴 No → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴) ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
5756adantr 480 . . 3 ((𝐴 No 𝐵 No ) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴) ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ dom 𝐴))
5851, 55, 573imtr4d 282 . 2 ((𝐴 No 𝐵 No ) → ((( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴)))
5958imp 444 1 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ⊆ wss 3540  ∩ cint 4410   class class class wbr 4583  dom cdm 5038  Ord word 5639  Oncon0 5640  Fun wfun 5798  ‘cfv 5804   No csur 31037
 Copyright terms: Public domain W3C validator