Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  onov0suclim Structured version   Visualization version   GIF version

Theorem onov0suclim 43263
Description: Compactly express rules for binary operations on ordinals. (Contributed by RP, 18-Jan-2025.)
Hypotheses
Ref Expression
onov0suclim.0 (𝐴 ∈ On → (𝐴 ∅) = 𝐷)
onov0suclim.suc ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 suc 𝐶) = 𝐸)
onov0suclim.lim (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 𝐵) = 𝐹)
Assertion
Ref Expression
onov0suclim ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))

Proof of Theorem onov0suclim
StepHypRef Expression
1 eloni 6395 . . . 4 (𝐵 ∈ On → Ord 𝐵)
2 orduniorsuc 7849 . . . . 5 (Ord 𝐵 → (𝐵 = 𝐵𝐵 = suc 𝐵))
3 unizlim 6508 . . . . . . 7 (Ord 𝐵 → (𝐵 = 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
43biimpd 229 . . . . . 6 (Ord 𝐵 → (𝐵 = 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
54orim1d 967 . . . . 5 (Ord 𝐵 → ((𝐵 = 𝐵𝐵 = suc 𝐵) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵)))
62, 5mpd 15 . . . 4 (Ord 𝐵 → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵))
71, 6syl 17 . . 3 (𝐵 ∈ On → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵))
87adantl 481 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵))
9 oveq2 7438 . . . . . . . . 9 (𝐵 = ∅ → (𝐴 𝐵) = (𝐴 ∅))
10 onov0suclim.0 . . . . . . . . 9 (𝐴 ∈ On → (𝐴 ∅) = 𝐷)
119, 10sylan9eqr 2796 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 𝐵) = 𝐷)
1211ex 412 . . . . . . 7 (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
1312ad2antrr 726 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
14 eloni 6395 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
15 0elsuc 7854 . . . . . . . . . . . . 13 (Ord 𝐶 → ∅ ∈ suc 𝐶)
1614, 15syl 17 . . . . . . . . . . . 12 (𝐶 ∈ On → ∅ ∈ suc 𝐶)
1716adantl 481 . . . . . . . . . . 11 ((𝐵 = suc 𝐶𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18 simpl 482 . . . . . . . . . . 11 ((𝐵 = suc 𝐶𝐶 ∈ On) → 𝐵 = suc 𝐶)
1917, 18eleqtrrd 2841 . . . . . . . . . 10 ((𝐵 = suc 𝐶𝐶 ∈ On) → ∅ ∈ 𝐵)
20 n0i 4345 . . . . . . . . . 10 (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
2119, 20syl 17 . . . . . . . . 9 ((𝐵 = suc 𝐶𝐶 ∈ On) → ¬ 𝐵 = ∅)
2221pm2.21d 121 . . . . . . . 8 ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐸))
2322adantl 481 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐸))
2423impancom 451 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
25 nlim0 6444 . . . . . . . . 9 ¬ Lim ∅
26 limeq 6397 . . . . . . . . 9 (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
2725, 26mtbiri 327 . . . . . . . 8 (𝐵 = ∅ → ¬ Lim 𝐵)
2827adantl 481 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
2928pm2.21d 121 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
3013, 24, 293jca 1127 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
3130ex 412 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
3227con2i 139 . . . . . . . 8 (Lim 𝐵 → ¬ 𝐵 = ∅)
3332adantl 481 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ¬ 𝐵 = ∅)
3433pm2.21d 121 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
35 limeq 6397 . . . . . . . . . . . 12 (𝐵 = suc 𝐶 → (Lim 𝐵 ↔ Lim suc 𝐶))
3635notbid 318 . . . . . . . . . . 11 (𝐵 = suc 𝐶 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶))
3736biimprd 248 . . . . . . . . . 10 (𝐵 = suc 𝐶 → (¬ Lim suc 𝐶 → ¬ Lim 𝐵))
38 nlimsucg 7862 . . . . . . . . . 10 (𝐶 ∈ On → ¬ Lim suc 𝐶)
3937, 38impel 505 . . . . . . . . 9 ((𝐵 = suc 𝐶𝐶 ∈ On) → ¬ Lim 𝐵)
4039adantl 481 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → ¬ Lim 𝐵)
4140pm2.21d 121 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (Lim 𝐵 → (𝐴 𝐵) = 𝐸))
4241impancom 451 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
43 onov0suclim.lim . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 𝐵) = 𝐹)
4443a1d 25 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
4534, 42, 443jca 1127 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
4645ex 412 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
4731, 46jaod 859 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
48 1n0 8524 . . . . . . . . 9 1o ≠ ∅
49 necom 2991 . . . . . . . . . . 11 (1o ≠ ∅ ↔ ∅ ≠ 1o)
50 df-1o 8504 . . . . . . . . . . . . 13 1o = suc ∅
51 uni0 4939 . . . . . . . . . . . . . 14 ∅ = ∅
52 suceq 6451 . . . . . . . . . . . . . 14 ( ∅ = ∅ → suc ∅ = suc ∅)
5351, 52ax-mp 5 . . . . . . . . . . . . 13 suc ∅ = suc ∅
5450, 53eqtr4i 2765 . . . . . . . . . . . 12 1o = suc
5554neeq2i 3003 . . . . . . . . . . 11 (∅ ≠ 1o ↔ ∅ ≠ suc ∅)
56 df-ne 2938 . . . . . . . . . . 11 (∅ ≠ suc ∅ ↔ ¬ ∅ = suc ∅)
5749, 55, 563bitri 297 . . . . . . . . . 10 (1o ≠ ∅ ↔ ¬ ∅ = suc ∅)
58 id 22 . . . . . . . . . . . 12 (𝐵 = ∅ → 𝐵 = ∅)
59 unieq 4922 . . . . . . . . . . . . 13 (𝐵 = ∅ → 𝐵 = ∅)
60 suceq 6451 . . . . . . . . . . . . 13 ( 𝐵 = ∅ → suc 𝐵 = suc ∅)
6159, 60syl 17 . . . . . . . . . . . 12 (𝐵 = ∅ → suc 𝐵 = suc ∅)
6258, 61eqeq12d 2750 . . . . . . . . . . 11 (𝐵 = ∅ → (𝐵 = suc 𝐵 ↔ ∅ = suc ∅))
6362notbid 318 . . . . . . . . . 10 (𝐵 = ∅ → (¬ 𝐵 = suc 𝐵 ↔ ¬ ∅ = suc ∅))
6457, 63bitr4id 290 . . . . . . . . 9 (𝐵 = ∅ → (1o ≠ ∅ ↔ ¬ 𝐵 = suc 𝐵))
6548, 64mpbii 233 . . . . . . . 8 (𝐵 = ∅ → ¬ 𝐵 = suc 𝐵)
6665con2i 139 . . . . . . 7 (𝐵 = suc 𝐵 → ¬ 𝐵 = ∅)
6766adantl 481 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ¬ 𝐵 = ∅)
6867pm2.21d 121 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
69 simprl 771 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → 𝐵 = suc 𝐶)
7069oveq2d 7446 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 𝐵) = (𝐴 suc 𝐶))
71 onov0suclim.suc . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 suc 𝐶) = 𝐸)
7271adantrl 716 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 suc 𝐶) = 𝐸)
7370, 72eqtrd 2774 . . . . . . 7 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 𝐵) = 𝐸)
7473ex 412 . . . . . 6 (𝐴 ∈ On → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
7574ad2antrr 726 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
76 onuni 7807 . . . . . . . . 9 (𝐵 ∈ On → 𝐵 ∈ On)
77 nlimsucg 7862 . . . . . . . . 9 ( 𝐵 ∈ On → ¬ Lim suc 𝐵)
7876, 77syl 17 . . . . . . . 8 (𝐵 ∈ On → ¬ Lim suc 𝐵)
79 limeq 6397 . . . . . . . . . 10 (𝐵 = suc 𝐵 → (Lim 𝐵 ↔ Lim suc 𝐵))
8079notbid 318 . . . . . . . . 9 (𝐵 = suc 𝐵 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐵))
8180biimprd 248 . . . . . . . 8 (𝐵 = suc 𝐵 → (¬ Lim suc 𝐵 → ¬ Lim 𝐵))
8278, 81mpan9 506 . . . . . . 7 ((𝐵 ∈ On ∧ 𝐵 = suc 𝐵) → ¬ Lim 𝐵)
8382adantll 714 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ¬ Lim 𝐵)
8483pm2.21d 121 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
8568, 75, 843jca 1127 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
8685ex 412 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc 𝐵 → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
8747, 86jaod 859 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
888, 87mpd 15 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  wne 2937  c0 4338   cuni 4911  Ord word 6384  Oncon0 6385  Lim wlim 6386  suc csuc 6387  (class class class)co 7430  1oc1o 8497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-11 2154  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fv 6570  df-ov 7433  df-1o 8504
This theorem is referenced by:  oa0suclim  43264  om0suclim  43265  oe0suclim  43266
  Copyright terms: Public domain W3C validator