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 41895
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 6366 . . . 4 (𝐵 ∈ On → Ord 𝐵)
2 orduniorsuc 7805 . . . . 5 (Ord 𝐵 → (𝐵 = 𝐵𝐵 = suc 𝐵))
3 unizlim 6479 . . . . . . 7 (Ord 𝐵 → (𝐵 = 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
43biimpd 228 . . . . . 6 (Ord 𝐵 → (𝐵 = 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
54orim1d 965 . . . . 5 (Ord 𝐵 → ((𝐵 = 𝐵𝐵 = suc 𝐵) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵)))
62, 5mpd 15 . . . 4 (Ord 𝐵 → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵))
71, 6syl 17 . . 3 (𝐵 ∈ On → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵))
87adantl 483 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) ∨ 𝐵 = suc 𝐵))
9 oveq2 7404 . . . . . . . . 9 (𝐵 = ∅ → (𝐴 𝐵) = (𝐴 ∅))
10 onov0suclim.0 . . . . . . . . 9 (𝐴 ∈ On → (𝐴 ∅) = 𝐷)
119, 10sylan9eqr 2795 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 𝐵) = 𝐷)
1211ex 414 . . . . . . 7 (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
1312ad2antrr 725 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
14 eloni 6366 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
15 0elsuc 7810 . . . . . . . . . . . . 13 (Ord 𝐶 → ∅ ∈ suc 𝐶)
1614, 15syl 17 . . . . . . . . . . . 12 (𝐶 ∈ On → ∅ ∈ suc 𝐶)
1716adantl 483 . . . . . . . . . . 11 ((𝐵 = suc 𝐶𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18 simpl 484 . . . . . . . . . . 11 ((𝐵 = suc 𝐶𝐶 ∈ On) → 𝐵 = suc 𝐶)
1917, 18eleqtrrd 2837 . . . . . . . . . 10 ((𝐵 = suc 𝐶𝐶 ∈ On) → ∅ ∈ 𝐵)
20 n0i 4331 . . . . . . . . . 10 (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
2119, 20syl 17 . . . . . . . . 9 ((𝐵 = suc 𝐶𝐶 ∈ On) → ¬ 𝐵 = ∅)
2221pm2.21d 121 . . . . . . . 8 ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐸))
2322adantl 483 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐸))
2423impancom 453 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
25 nlim0 6415 . . . . . . . . 9 ¬ Lim ∅
26 limeq 6368 . . . . . . . . 9 (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
2725, 26mtbiri 327 . . . . . . . 8 (𝐵 = ∅ → ¬ Lim 𝐵)
2827adantl 483 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
2928pm2.21d 121 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
3013, 24, 293jca 1129 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
3130ex 414 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
3227con2i 139 . . . . . . . 8 (Lim 𝐵 → ¬ 𝐵 = ∅)
3332adantl 483 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ¬ 𝐵 = ∅)
3433pm2.21d 121 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
35 limeq 6368 . . . . . . . . . . . 12 (𝐵 = suc 𝐶 → (Lim 𝐵 ↔ Lim suc 𝐶))
3635notbid 318 . . . . . . . . . . 11 (𝐵 = suc 𝐶 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶))
3736biimprd 247 . . . . . . . . . 10 (𝐵 = suc 𝐶 → (¬ Lim suc 𝐶 → ¬ Lim 𝐵))
38 nlimsucg 7818 . . . . . . . . . 10 (𝐶 ∈ On → ¬ Lim suc 𝐶)
3937, 38impel 507 . . . . . . . . 9 ((𝐵 = suc 𝐶𝐶 ∈ On) → ¬ Lim 𝐵)
4039adantl 483 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → ¬ Lim 𝐵)
4140pm2.21d 121 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (Lim 𝐵 → (𝐴 𝐵) = 𝐸))
4241impancom 453 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
43 onov0suclim.lim . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 𝐵) = 𝐹)
4443a1d 25 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
4534, 42, 443jca 1129 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
4645ex 414 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
4731, 46jaod 858 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
48 1n0 8475 . . . . . . . . 9 1o ≠ ∅
49 necom 2995 . . . . . . . . . . 11 (1o ≠ ∅ ↔ ∅ ≠ 1o)
50 df-1o 8453 . . . . . . . . . . . . 13 1o = suc ∅
51 uni0 4935 . . . . . . . . . . . . . 14 ∅ = ∅
52 suceq 6422 . . . . . . . . . . . . . 14 ( ∅ = ∅ → suc ∅ = suc ∅)
5351, 52ax-mp 5 . . . . . . . . . . . . 13 suc ∅ = suc ∅
5450, 53eqtr4i 2764 . . . . . . . . . . . 12 1o = suc
5554neeq2i 3007 . . . . . . . . . . 11 (∅ ≠ 1o ↔ ∅ ≠ suc ∅)
56 df-ne 2942 . . . . . . . . . . 11 (∅ ≠ suc ∅ ↔ ¬ ∅ = suc ∅)
5749, 55, 563bitri 297 . . . . . . . . . 10 (1o ≠ ∅ ↔ ¬ ∅ = suc ∅)
58 id 22 . . . . . . . . . . . 12 (𝐵 = ∅ → 𝐵 = ∅)
59 unieq 4915 . . . . . . . . . . . . 13 (𝐵 = ∅ → 𝐵 = ∅)
60 suceq 6422 . . . . . . . . . . . . 13 ( 𝐵 = ∅ → suc 𝐵 = suc ∅)
6159, 60syl 17 . . . . . . . . . . . 12 (𝐵 = ∅ → suc 𝐵 = suc ∅)
6258, 61eqeq12d 2749 . . . . . . . . . . 11 (𝐵 = ∅ → (𝐵 = suc 𝐵 ↔ ∅ = suc ∅))
6362notbid 318 . . . . . . . . . 10 (𝐵 = ∅ → (¬ 𝐵 = suc 𝐵 ↔ ¬ ∅ = suc ∅))
6457, 63bitr4id 290 . . . . . . . . 9 (𝐵 = ∅ → (1o ≠ ∅ ↔ ¬ 𝐵 = suc 𝐵))
6548, 64mpbii 232 . . . . . . . 8 (𝐵 = ∅ → ¬ 𝐵 = suc 𝐵)
6665con2i 139 . . . . . . 7 (𝐵 = suc 𝐵 → ¬ 𝐵 = ∅)
6766adantl 483 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ¬ 𝐵 = ∅)
6867pm2.21d 121 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
69 simprl 770 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → 𝐵 = suc 𝐶)
7069oveq2d 7412 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 𝐵) = (𝐴 suc 𝐶))
71 onov0suclim.suc . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 suc 𝐶) = 𝐸)
7271adantrl 715 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 suc 𝐶) = 𝐸)
7370, 72eqtrd 2773 . . . . . . 7 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 𝐵) = 𝐸)
7473ex 414 . . . . . 6 (𝐴 ∈ On → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
7574ad2antrr 725 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
76 onuni 7763 . . . . . . . . 9 (𝐵 ∈ On → 𝐵 ∈ On)
77 nlimsucg 7818 . . . . . . . . 9 ( 𝐵 ∈ On → ¬ Lim suc 𝐵)
7876, 77syl 17 . . . . . . . 8 (𝐵 ∈ On → ¬ Lim suc 𝐵)
79 limeq 6368 . . . . . . . . . 10 (𝐵 = suc 𝐵 → (Lim 𝐵 ↔ Lim suc 𝐵))
8079notbid 318 . . . . . . . . 9 (𝐵 = suc 𝐵 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐵))
8180biimprd 247 . . . . . . . 8 (𝐵 = suc 𝐵 → (¬ Lim suc 𝐵 → ¬ Lim 𝐵))
8278, 81mpan9 508 . . . . . . 7 ((𝐵 ∈ On ∧ 𝐵 = suc 𝐵) → ¬ Lim 𝐵)
8382adantll 713 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ¬ Lim 𝐵)
8483pm2.21d 121 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
8568, 75, 843jca 1129 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
8685ex 414 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc 𝐵 → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
8747, 86jaod 858 . 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 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wne 2941  c0 4320   cuni 4904  Ord word 6355  Oncon0 6356  Lim wlim 6357  suc csuc 6358  (class class class)co 7396  1oc1o 8446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704  ax-sep 5295  ax-nul 5302  ax-pr 5423  ax-un 7712
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-br 5145  df-opab 5207  df-tr 5262  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fv 6543  df-ov 7399  df-1o 8453
This theorem is referenced by:  oa0suclim  41896  om0suclim  41897  oe0suclim  41898
  Copyright terms: Public domain W3C validator