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 43287
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 6394 . . . 4 (𝐵 ∈ On → Ord 𝐵)
2 orduniorsuc 7850 . . . . 5 (Ord 𝐵 → (𝐵 = 𝐵𝐵 = suc 𝐵))
3 unizlim 6507 . . . . . . 7 (Ord 𝐵 → (𝐵 = 𝐵 ↔ (𝐵 = ∅ ∨ Lim 𝐵)))
43biimpd 229 . . . . . 6 (Ord 𝐵 → (𝐵 = 𝐵 → (𝐵 = ∅ ∨ Lim 𝐵)))
54orim1d 968 . . . . 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 7439 . . . . . . . . 9 (𝐵 = ∅ → (𝐴 𝐵) = (𝐴 ∅))
10 onov0suclim.0 . . . . . . . . 9 (𝐴 ∈ On → (𝐴 ∅) = 𝐷)
119, 10sylan9eqr 2799 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 𝐵) = 𝐷)
1211ex 412 . . . . . . 7 (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
1312ad2antrr 726 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (𝐵 = ∅ → (𝐴 𝐵) = 𝐷))
14 eloni 6394 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
15 0elsuc 7855 . . . . . . . . . . . . 13 (Ord 𝐶 → ∅ ∈ suc 𝐶)
1614, 15syl 17 . . . . . . . . . . . 12 (𝐶 ∈ On → ∅ ∈ suc 𝐶)
1716adantl 481 . . . . . . . . . . 11 ((𝐵 = suc 𝐶𝐶 ∈ On) → ∅ ∈ suc 𝐶)
18 simpl 482 . . . . . . . . . . 11 ((𝐵 = suc 𝐶𝐶 ∈ On) → 𝐵 = suc 𝐶)
1917, 18eleqtrrd 2844 . . . . . . . . . 10 ((𝐵 = suc 𝐶𝐶 ∈ On) → ∅ ∈ 𝐵)
20 n0i 4340 . . . . . . . . . 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 6443 . . . . . . . . 9 ¬ Lim ∅
26 limeq 6396 . . . . . . . . 9 (𝐵 = ∅ → (Lim 𝐵 ↔ Lim ∅))
2725, 26mtbiri 327 . . . . . . . 8 (𝐵 = ∅ → ¬ Lim 𝐵)
2827adantl 481 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → ¬ Lim 𝐵)
2928pm2.21d 121 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = ∅) → (Lim 𝐵 → (𝐴 𝐵) = 𝐹))
3013, 24, 293jca 1129 . . . . 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 6396 . . . . . . . . . . . 12 (𝐵 = suc 𝐶 → (Lim 𝐵 ↔ Lim suc 𝐶))
3635notbid 318 . . . . . . . . . . 11 (𝐵 = suc 𝐶 → (¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶))
3736biimprd 248 . . . . . . . . . 10 (𝐵 = suc 𝐶 → (¬ Lim suc 𝐶 → ¬ Lim 𝐵))
38 nlimsucg 7863 . . . . . . . . . 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 1129 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
4645ex 412 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝐵 → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
4731, 46jaod 860 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ ∨ Lim 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
48 1n0 8526 . . . . . . . . 9 1o ≠ ∅
49 necom 2994 . . . . . . . . . . 11 (1o ≠ ∅ ↔ ∅ ≠ 1o)
50 df-1o 8506 . . . . . . . . . . . . 13 1o = suc ∅
51 uni0 4935 . . . . . . . . . . . . . 14 ∅ = ∅
52 suceq 6450 . . . . . . . . . . . . . 14 ( ∅ = ∅ → suc ∅ = suc ∅)
5351, 52ax-mp 5 . . . . . . . . . . . . 13 suc ∅ = suc ∅
5450, 53eqtr4i 2768 . . . . . . . . . . . 12 1o = suc
5554neeq2i 3006 . . . . . . . . . . 11 (∅ ≠ 1o ↔ ∅ ≠ suc ∅)
56 df-ne 2941 . . . . . . . . . . 11 (∅ ≠ suc ∅ ↔ ¬ ∅ = suc ∅)
5749, 55, 563bitri 297 . . . . . . . . . 10 (1o ≠ ∅ ↔ ¬ ∅ = suc ∅)
58 id 22 . . . . . . . . . . . 12 (𝐵 = ∅ → 𝐵 = ∅)
59 unieq 4918 . . . . . . . . . . . . 13 (𝐵 = ∅ → 𝐵 = ∅)
60 suceq 6450 . . . . . . . . . . . . 13 ( 𝐵 = ∅ → suc 𝐵 = suc ∅)
6159, 60syl 17 . . . . . . . . . . . 12 (𝐵 = ∅ → suc 𝐵 = suc ∅)
6258, 61eqeq12d 2753 . . . . . . . . . . 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 7447 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 𝐵) = (𝐴 suc 𝐶))
71 onov0suclim.suc . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 suc 𝐶) = 𝐸)
7271adantrl 716 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 suc 𝐶) = 𝐸)
7370, 72eqtrd 2777 . . . . . . 7 ((𝐴 ∈ On ∧ (𝐵 = suc 𝐶𝐶 ∈ On)) → (𝐴 𝐵) = 𝐸)
7473ex 412 . . . . . 6 (𝐴 ∈ On → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
7574ad2antrr 726 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸))
76 onuni 7808 . . . . . . . . 9 (𝐵 ∈ On → 𝐵 ∈ On)
77 nlimsucg 7863 . . . . . . . . 9 ( 𝐵 ∈ On → ¬ Lim suc 𝐵)
7876, 77syl 17 . . . . . . . 8 (𝐵 ∈ On → ¬ Lim suc 𝐵)
79 limeq 6396 . . . . . . . . . 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 1129 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 = suc 𝐵) → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹)))
8685ex 412 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = suc 𝐵 → ((𝐵 = ∅ → (𝐴 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶𝐶 ∈ On) → (𝐴 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 𝐵) = 𝐹))))
8747, 86jaod 860 . 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 848  w3a 1087   = wceq 1540  wcel 2108  wne 2940  c0 4333   cuni 4907  Ord word 6383  Oncon0 6384  Lim wlim 6385  suc csuc 6386  (class class class)co 7431  1oc1o 8499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fv 6569  df-ov 7434  df-1o 8506
This theorem is referenced by:  oa0suclim  43288  om0suclim  43289  oe0suclim  43290
  Copyright terms: Public domain W3C validator