MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  onuninsuci Structured version   Visualization version   GIF version

Theorem onuninsuci 7861
Description: An ordinal is equal to its union if and only if it is not the successor of an ordinal. A closed-form generalization of this result is orduninsuc 7864. (Contributed by NM, 18-Feb-2004.)
Hypothesis
Ref Expression
onssi.1 𝐴 ∈ On
Assertion
Ref Expression
onuninsuci (𝐴 = 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Distinct variable group:   𝑥,𝐴

Proof of Theorem onuninsuci
StepHypRef Expression
1 onssi.1 . . . . . . 7 𝐴 ∈ On
21onirri 6499 . . . . . 6 ¬ 𝐴𝐴
3 id 22 . . . . . . . 8 (𝐴 = 𝐴𝐴 = 𝐴)
4 df-suc 6392 . . . . . . . . . . . 12 suc 𝑥 = (𝑥 ∪ {𝑥})
54eqeq2i 2748 . . . . . . . . . . 11 (𝐴 = suc 𝑥𝐴 = (𝑥 ∪ {𝑥}))
6 unieq 4923 . . . . . . . . . . 11 (𝐴 = (𝑥 ∪ {𝑥}) → 𝐴 = (𝑥 ∪ {𝑥}))
75, 6sylbi 217 . . . . . . . . . 10 (𝐴 = suc 𝑥 𝐴 = (𝑥 ∪ {𝑥}))
8 uniun 4935 . . . . . . . . . . 11 (𝑥 ∪ {𝑥}) = ( 𝑥 {𝑥})
9 unisnv 4932 . . . . . . . . . . . 12 {𝑥} = 𝑥
109uneq2i 4175 . . . . . . . . . . 11 ( 𝑥 {𝑥}) = ( 𝑥𝑥)
118, 10eqtri 2763 . . . . . . . . . 10 (𝑥 ∪ {𝑥}) = ( 𝑥𝑥)
127, 11eqtrdi 2791 . . . . . . . . 9 (𝐴 = suc 𝑥 𝐴 = ( 𝑥𝑥))
13 tron 6409 . . . . . . . . . . . 12 Tr On
14 eleq1 2827 . . . . . . . . . . . . 13 (𝐴 = suc 𝑥 → (𝐴 ∈ On ↔ suc 𝑥 ∈ On))
151, 14mpbii 233 . . . . . . . . . . . 12 (𝐴 = suc 𝑥 → suc 𝑥 ∈ On)
16 trsuc 6473 . . . . . . . . . . . 12 ((Tr On ∧ suc 𝑥 ∈ On) → 𝑥 ∈ On)
1713, 15, 16sylancr 587 . . . . . . . . . . 11 (𝐴 = suc 𝑥𝑥 ∈ On)
18 ontr 6495 . . . . . . . . . . . 12 (𝑥 ∈ On → Tr 𝑥)
19 df-tr 5266 . . . . . . . . . . . 12 (Tr 𝑥 𝑥𝑥)
2018, 19sylib 218 . . . . . . . . . . 11 (𝑥 ∈ On → 𝑥𝑥)
2117, 20syl 17 . . . . . . . . . 10 (𝐴 = suc 𝑥 𝑥𝑥)
22 ssequn1 4196 . . . . . . . . . 10 ( 𝑥𝑥 ↔ ( 𝑥𝑥) = 𝑥)
2321, 22sylib 218 . . . . . . . . 9 (𝐴 = suc 𝑥 → ( 𝑥𝑥) = 𝑥)
2412, 23eqtrd 2775 . . . . . . . 8 (𝐴 = suc 𝑥 𝐴 = 𝑥)
253, 24sylan9eqr 2797 . . . . . . 7 ((𝐴 = suc 𝑥𝐴 = 𝐴) → 𝐴 = 𝑥)
26 vex 3482 . . . . . . . . . 10 𝑥 ∈ V
2726sucid 6468 . . . . . . . . 9 𝑥 ∈ suc 𝑥
28 eleq2 2828 . . . . . . . . 9 (𝐴 = suc 𝑥 → (𝑥𝐴𝑥 ∈ suc 𝑥))
2927, 28mpbiri 258 . . . . . . . 8 (𝐴 = suc 𝑥𝑥𝐴)
3029adantr 480 . . . . . . 7 ((𝐴 = suc 𝑥𝐴 = 𝐴) → 𝑥𝐴)
3125, 30eqeltrd 2839 . . . . . 6 ((𝐴 = suc 𝑥𝐴 = 𝐴) → 𝐴𝐴)
322, 31mto 197 . . . . 5 ¬ (𝐴 = suc 𝑥𝐴 = 𝐴)
3332imnani 400 . . . 4 (𝐴 = suc 𝑥 → ¬ 𝐴 = 𝐴)
3433rexlimivw 3149 . . 3 (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ 𝐴 = 𝐴)
35 onuni 7808 . . . . 5 (𝐴 ∈ On → 𝐴 ∈ On)
361, 35ax-mp 5 . . . 4 𝐴 ∈ On
37 onuniorsuc 7857 . . . . . 6 (𝐴 ∈ On → (𝐴 = 𝐴𝐴 = suc 𝐴))
381, 37ax-mp 5 . . . . 5 (𝐴 = 𝐴𝐴 = suc 𝐴)
3938ori 861 . . . 4 𝐴 = 𝐴𝐴 = suc 𝐴)
40 suceq 6452 . . . . 5 (𝑥 = 𝐴 → suc 𝑥 = suc 𝐴)
4140rspceeqv 3645 . . . 4 (( 𝐴 ∈ On ∧ 𝐴 = suc 𝐴) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)
4236, 39, 41sylancr 587 . . 3 𝐴 = 𝐴 → ∃𝑥 ∈ On 𝐴 = suc 𝑥)
4334, 42impbii 209 . 2 (∃𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ¬ 𝐴 = 𝐴)
4443con2bii 357 1 (𝐴 = 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wrex 3068  cun 3961  wss 3963  {csn 4631   cuni 4912  Tr wtr 5265  Oncon0 6386  suc csuc 6388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-suc 6392
This theorem is referenced by:  orduninsuc  7864
  Copyright terms: Public domain W3C validator