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

Theorem omcl 8557
Description: Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. Remark 2.8 of [Schloeder] p. 5. (Contributed by NM, 3-Aug-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
omcl ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On)

Proof of Theorem omcl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7427 . . . 4 (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o ∅))
21eleq1d 2810 . . 3 (𝑥 = ∅ → ((𝐴 ·o 𝑥) ∈ On ↔ (𝐴 ·o ∅) ∈ On))
3 oveq2 7427 . . . 4 (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦))
43eleq1d 2810 . . 3 (𝑥 = 𝑦 → ((𝐴 ·o 𝑥) ∈ On ↔ (𝐴 ·o 𝑦) ∈ On))
5 oveq2 7427 . . . 4 (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦))
65eleq1d 2810 . . 3 (𝑥 = suc 𝑦 → ((𝐴 ·o 𝑥) ∈ On ↔ (𝐴 ·o suc 𝑦) ∈ On))
7 oveq2 7427 . . . 4 (𝑥 = 𝐵 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐵))
87eleq1d 2810 . . 3 (𝑥 = 𝐵 → ((𝐴 ·o 𝑥) ∈ On ↔ (𝐴 ·o 𝐵) ∈ On))
9 om0 8538 . . . 4 (𝐴 ∈ On → (𝐴 ·o ∅) = ∅)
10 0elon 6425 . . . 4 ∅ ∈ On
119, 10eqeltrdi 2833 . . 3 (𝐴 ∈ On → (𝐴 ·o ∅) ∈ On)
12 oacl 8556 . . . . . . 7 (((𝐴 ·o 𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·o 𝑦) +o 𝐴) ∈ On)
1312expcom 412 . . . . . 6 (𝐴 ∈ On → ((𝐴 ·o 𝑦) ∈ On → ((𝐴 ·o 𝑦) +o 𝐴) ∈ On))
1413adantr 479 . . . . 5 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝑦) ∈ On → ((𝐴 ·o 𝑦) +o 𝐴) ∈ On))
15 omsuc 8547 . . . . . 6 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴))
1615eleq1d 2810 . . . . 5 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o suc 𝑦) ∈ On ↔ ((𝐴 ·o 𝑦) +o 𝐴) ∈ On))
1714, 16sylibrd 258 . . . 4 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝑦) ∈ On → (𝐴 ·o suc 𝑦) ∈ On))
1817expcom 412 . . 3 (𝑦 ∈ On → (𝐴 ∈ On → ((𝐴 ·o 𝑦) ∈ On → (𝐴 ·o suc 𝑦) ∈ On)))
19 vex 3465 . . . . . 6 𝑥 ∈ V
20 iunon 8360 . . . . . 6 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (𝐴 ·o 𝑦) ∈ On) → 𝑦𝑥 (𝐴 ·o 𝑦) ∈ On)
2119, 20mpan 688 . . . . 5 (∀𝑦𝑥 (𝐴 ·o 𝑦) ∈ On → 𝑦𝑥 (𝐴 ·o 𝑦) ∈ On)
22 omlim 8554 . . . . . . 7 ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ·o 𝑥) = 𝑦𝑥 (𝐴 ·o 𝑦))
2319, 22mpanr1 701 . . . . . 6 ((𝐴 ∈ On ∧ Lim 𝑥) → (𝐴 ·o 𝑥) = 𝑦𝑥 (𝐴 ·o 𝑦))
2423eleq1d 2810 . . . . 5 ((𝐴 ∈ On ∧ Lim 𝑥) → ((𝐴 ·o 𝑥) ∈ On ↔ 𝑦𝑥 (𝐴 ·o 𝑦) ∈ On))
2521, 24imbitrrid 245 . . . 4 ((𝐴 ∈ On ∧ Lim 𝑥) → (∀𝑦𝑥 (𝐴 ·o 𝑦) ∈ On → (𝐴 ·o 𝑥) ∈ On))
2625expcom 412 . . 3 (Lim 𝑥 → (𝐴 ∈ On → (∀𝑦𝑥 (𝐴 ·o 𝑦) ∈ On → (𝐴 ·o 𝑥) ∈ On)))
272, 4, 6, 8, 11, 18, 26tfinds3 7870 . 2 (𝐵 ∈ On → (𝐴 ∈ On → (𝐴 ·o 𝐵) ∈ On))
2827impcom 406 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wcel 2098  wral 3050  Vcvv 3461  c0 4322   ciun 4997  Oncon0 6371  Lim wlim 6372  suc csuc 6373  (class class class)co 7419   +o coa 8484   ·o comu 8485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-oadd 8491  df-omul 8492
This theorem is referenced by:  oecl  8558  omordi  8587  omord2  8588  omcan  8590  omword  8591  omwordri  8593  om00  8596  om00el  8597  omlimcl  8599  odi  8600  omass  8601  oneo  8602  omeulem1  8603  omeulem2  8604  omopth2  8605  oeoelem  8619  oeoe  8620  oeeui  8623  oaabs2  8670  omxpenlem  9098  omxpen  9099  cantnfle  9696  cantnflt  9697  cantnflem1d  9713  cantnflem1  9714  cantnflem3  9716  cantnflem4  9717  cnfcomlem  9724  xpnum  9976  infxpenc  10043  dfac12lem2  10169  onexomgt  42811  omlimcl2  42812  onexlimgt  42813  onexoegt  42814  oaomoecl  42849  oaabsb  42865  dflim5  42900  omabs2  42903  naddwordnexlem0  42968  naddwordnexlem1  42969  naddwordnexlem3  42971  oawordex3  42972  naddwordnexlem4  42973
  Copyright terms: Public domain W3C validator