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

Definition df-oexp 8419
Description: Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.)
Assertion
Ref Expression
df-oexp โ†‘o = (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ if(๐‘ฅ = โˆ…, (1o โˆ– ๐‘ฆ), (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ)))
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘ง

Detailed syntax breakdown of Definition df-oexp
StepHypRef Expression
1 coe 8412 . 2 class โ†‘o
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 con0 6318 . . 3 class On
52cv 1541 . . . . 5 class ๐‘ฅ
6 c0 4283 . . . . 5 class โˆ…
75, 6wceq 1542 . . . 4 wff ๐‘ฅ = โˆ…
8 c1o 8406 . . . . 5 class 1o
93cv 1541 . . . . 5 class ๐‘ฆ
108, 9cdif 3908 . . . 4 class (1o โˆ– ๐‘ฆ)
11 vz . . . . . . 7 setvar ๐‘ง
12 cvv 3446 . . . . . . 7 class V
1311cv 1541 . . . . . . . 8 class ๐‘ง
14 comu 8411 . . . . . . . 8 class ยทo
1513, 5, 14co 7358 . . . . . . 7 class (๐‘ง ยทo ๐‘ฅ)
1611, 12, 15cmpt 5189 . . . . . 6 class (๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ))
1716, 8crdg 8356 . . . . 5 class rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)
189, 17cfv 6497 . . . 4 class (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ)
197, 10, 18cif 4487 . . 3 class if(๐‘ฅ = โˆ…, (1o โˆ– ๐‘ฆ), (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ))
202, 3, 4, 4, 19cmpo 7360 . 2 class (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ if(๐‘ฅ = โˆ…, (1o โˆ– ๐‘ฆ), (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ)))
211, 20wceq 1542 1 wff โ†‘o = (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ if(๐‘ฅ = โˆ…, (1o โˆ– ๐‘ฆ), (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ)))
Colors of variables: wff setvar class
This definition is referenced by:  fnoe  8457  oev  8461
  Copyright terms: Public domain W3C validator