Description: Ordinal multiplication with zero. Definition 8.15(a) of TakeutiZaring p. 62. See om0x for a way to remove the antecedent A e. On . (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 8-Sep-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | om0 | |- ( A e. On -> ( A .o (/) ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0elon | |- (/) e. On |
|
| 2 | omv | |- ( ( A e. On /\ (/) e. On ) -> ( A .o (/) ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` (/) ) ) |
|
| 3 | 1 2 | mpan2 | |- ( A e. On -> ( A .o (/) ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` (/) ) ) |
| 4 | 0ex | |- (/) e. _V |
|
| 5 | 4 | rdg0 | |- ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` (/) ) = (/) |
| 6 | 3 5 | eqtrdi | |- ( A e. On -> ( A .o (/) ) = (/) ) |