Theorem om0

Description: Ordinal multiplication with zero. Definition 8.15(a) of TakeutiZaring p. 62. Definition 2.5 of Schloeder p. 4. 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 ∅ ) = ∅ )

Proof

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 ∅ ) = ∅ )