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

Theorem nodenselem4 31083
 Description: Lemma for nodense 31088. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
Assertion
Ref Expression
nodenselem4 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem nodenselem4
StepHypRef Expression
1 ssrab2 3650 . 2 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On
2 sltirr 31069 . . . . . . 7 (𝐴 No → ¬ 𝐴 <s 𝐴)
3 breq2 4587 . . . . . . . . 9 (𝐴 = 𝐵 → (𝐴 <s 𝐴𝐴 <s 𝐵))
43biimprcd 239 . . . . . . . 8 (𝐴 <s 𝐵 → (𝐴 = 𝐵𝐴 <s 𝐴))
54con3d 147 . . . . . . 7 (𝐴 <s 𝐵 → (¬ 𝐴 <s 𝐴 → ¬ 𝐴 = 𝐵))
62, 5syl5com 31 . . . . . 6 (𝐴 No → (𝐴 <s 𝐵 → ¬ 𝐴 = 𝐵))
76adantr 480 . . . . 5 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 → ¬ 𝐴 = 𝐵))
8 nofnbday 31049 . . . . . . . 8 (𝐴 No 𝐴 Fn ( bday 𝐴))
9 nofnbday 31049 . . . . . . . 8 (𝐵 No 𝐵 Fn ( bday 𝐵))
10 eqfnfv2 6220 . . . . . . . 8 ((𝐴 Fn ( bday 𝐴) ∧ 𝐵 Fn ( bday 𝐵)) → (𝐴 = 𝐵 ↔ (( bday 𝐴) = ( bday 𝐵) ∧ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎))))
118, 9, 10syl2an 493 . . . . . . 7 ((𝐴 No 𝐵 No ) → (𝐴 = 𝐵 ↔ (( bday 𝐴) = ( bday 𝐵) ∧ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎))))
1211notbid 307 . . . . . 6 ((𝐴 No 𝐵 No ) → (¬ 𝐴 = 𝐵 ↔ ¬ (( bday 𝐴) = ( bday 𝐵) ∧ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎))))
13 ianor 508 . . . . . . 7 (¬ (( bday 𝐴) = ( bday 𝐵) ∧ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎)) ↔ (¬ ( bday 𝐴) = ( bday 𝐵) ∨ ¬ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎)))
14 bdayelon 31079 . . . . . . . . . . . 12 ( bday 𝐴) ∈ On
1514onordi 5749 . . . . . . . . . . 11 Ord ( bday 𝐴)
16 bdayelon 31079 . . . . . . . . . . . 12 ( bday 𝐵) ∈ On
1716onordi 5749 . . . . . . . . . . 11 Ord ( bday 𝐵)
18 ordtri3 5676 . . . . . . . . . . 11 ((Ord ( bday 𝐴) ∧ Ord ( bday 𝐵)) → (( bday 𝐴) = ( bday 𝐵) ↔ ¬ (( bday 𝐴) ∈ ( bday 𝐵) ∨ ( bday 𝐵) ∈ ( bday 𝐴))))
1915, 17, 18mp2an 704 . . . . . . . . . 10 (( bday 𝐴) = ( bday 𝐵) ↔ ¬ (( bday 𝐴) ∈ ( bday 𝐵) ∨ ( bday 𝐵) ∈ ( bday 𝐴)))
2019con2bii 346 . . . . . . . . 9 ((( bday 𝐴) ∈ ( bday 𝐵) ∨ ( bday 𝐵) ∈ ( bday 𝐴)) ↔ ¬ ( bday 𝐴) = ( bday 𝐵))
21 nodenselem3 31082 . . . . . . . . . 10 ((𝐴 No 𝐵 No ) → (( bday 𝐴) ∈ ( bday 𝐵) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
22 nodenselem3 31082 . . . . . . . . . . . 12 ((𝐵 No 𝐴 No ) → (( bday 𝐵) ∈ ( bday 𝐴) → ∃𝑎 ∈ On (𝐵𝑎) ≠ (𝐴𝑎)))
23 necom 2835 . . . . . . . . . . . . 13 ((𝐵𝑎) ≠ (𝐴𝑎) ↔ (𝐴𝑎) ≠ (𝐵𝑎))
2423rexbii 3023 . . . . . . . . . . . 12 (∃𝑎 ∈ On (𝐵𝑎) ≠ (𝐴𝑎) ↔ ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎))
2522, 24syl6ib 240 . . . . . . . . . . 11 ((𝐵 No 𝐴 No ) → (( bday 𝐵) ∈ ( bday 𝐴) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
2625ancoms 468 . . . . . . . . . 10 ((𝐴 No 𝐵 No ) → (( bday 𝐵) ∈ ( bday 𝐴) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
2721, 26jaod 394 . . . . . . . . 9 ((𝐴 No 𝐵 No ) → ((( bday 𝐴) ∈ ( bday 𝐵) ∨ ( bday 𝐵) ∈ ( bday 𝐴)) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
2820, 27syl5bir 232 . . . . . . . 8 ((𝐴 No 𝐵 No ) → (¬ ( bday 𝐴) = ( bday 𝐵) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
29 rexnal 2978 . . . . . . . . . 10 (∃𝑎 ∈ ( bday 𝐴) ¬ (𝐴𝑎) = (𝐵𝑎) ↔ ¬ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎))
3014onssi 6929 . . . . . . . . . . . 12 ( bday 𝐴) ⊆ On
31 ssrexv 3630 . . . . . . . . . . . 12 (( bday 𝐴) ⊆ On → (∃𝑎 ∈ ( bday 𝐴) ¬ (𝐴𝑎) = (𝐵𝑎) → ∃𝑎 ∈ On ¬ (𝐴𝑎) = (𝐵𝑎)))
3230, 31ax-mp 5 . . . . . . . . . . 11 (∃𝑎 ∈ ( bday 𝐴) ¬ (𝐴𝑎) = (𝐵𝑎) → ∃𝑎 ∈ On ¬ (𝐴𝑎) = (𝐵𝑎))
33 df-ne 2782 . . . . . . . . . . . 12 ((𝐴𝑎) ≠ (𝐵𝑎) ↔ ¬ (𝐴𝑎) = (𝐵𝑎))
3433rexbii 3023 . . . . . . . . . . 11 (∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎) ↔ ∃𝑎 ∈ On ¬ (𝐴𝑎) = (𝐵𝑎))
3532, 34sylibr 223 . . . . . . . . . 10 (∃𝑎 ∈ ( bday 𝐴) ¬ (𝐴𝑎) = (𝐵𝑎) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎))
3629, 35sylbir 224 . . . . . . . . 9 (¬ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎))
3736a1i 11 . . . . . . . 8 ((𝐴 No 𝐵 No ) → (¬ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
3828, 37jaod 394 . . . . . . 7 ((𝐴 No 𝐵 No ) → ((¬ ( bday 𝐴) = ( bday 𝐵) ∨ ¬ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎)) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
3913, 38syl5bi 231 . . . . . 6 ((𝐴 No 𝐵 No ) → (¬ (( bday 𝐴) = ( bday 𝐵) ∧ ∀𝑎 ∈ ( bday 𝐴)(𝐴𝑎) = (𝐵𝑎)) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
4012, 39sylbid 229 . . . . 5 ((𝐴 No 𝐵 No ) → (¬ 𝐴 = 𝐵 → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
417, 40syld 46 . . . 4 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎)))
4241imp 444 . . 3 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎))
43 rabn0 3912 . . 3 ({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅ ↔ ∃𝑎 ∈ On (𝐴𝑎) ≠ (𝐵𝑎))
4442, 43sylibr 223 . 2 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
45 oninton 6892 . 2 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
461, 44, 45sylancr 694 1 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ⊆ wss 3540  ∅c0 3874  ∩ cint 4410   class class class wbr 4583  Ord word 5639  Oncon0 5640   Fn wfn 5799  ‘cfv 5804   No csur 31037
 Copyright terms: Public domain W3C validator