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 | ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0elon | ⊢ ∅ ∈ On | |
2 | omv | ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 ·o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ ∅ ) ) | |
3 | 1 2 | mpan2 | ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ ∅ ) ) |
4 | 0ex | ⊢ ∅ ∈ V | |
5 | 4 | rdg0 | ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ ∅ ) = ∅ |
6 | 3 5 | eqtrdi | ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ ) |