Theorem om0r

Description: Ordinal multiplication with zero. Proposition 8.18(1) of TakeutiZaring p. 63. (Contributed by NM, 3-Aug-2004)

	Ref	Expression
Assertion	om0r	|- ( A e. On -> ( (/) .o A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( x = (/) -> ( (/) .o x ) = ( (/) .o (/) ) )
2	1	eqeq1d	|- ( x = (/) -> ( ( (/) .o x ) = (/) <-> ( (/) .o (/) ) = (/) ) )
3		oveq2	|- ( x = y -> ( (/) .o x ) = ( (/) .o y ) )
4	3	eqeq1d	|- ( x = y -> ( ( (/) .o x ) = (/) <-> ( (/) .o y ) = (/) ) )
5		oveq2	|- ( x = suc y -> ( (/) .o x ) = ( (/) .o suc y ) )
6	5	eqeq1d	|- ( x = suc y -> ( ( (/) .o x ) = (/) <-> ( (/) .o suc y ) = (/) ) )
7		oveq2	|- ( x = A -> ( (/) .o x ) = ( (/) .o A ) )
8	7	eqeq1d	|- ( x = A -> ( ( (/) .o x ) = (/) <-> ( (/) .o A ) = (/) ) )
9		0elon	|- (/) e. On
10		om0	|- ( (/) e. On -> ( (/) .o (/) ) = (/) )
11	9 10	ax-mp	|- ( (/) .o (/) ) = (/)
12		oveq1	|- ( ( (/) .o y ) = (/) -> ( ( (/) .o y ) +o (/) ) = ( (/) +o (/) ) )
13		omsuc	|- ( ( (/) e. On /\ y e. On ) -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) )
14	9 13	mpan	|- ( y e. On -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) )
15		oa0	|- ( (/) e. On -> ( (/) +o (/) ) = (/) )
16	9 15	ax-mp	|- ( (/) +o (/) ) = (/)
17	16	eqcomi	|- (/) = ( (/) +o (/) )
18	17	a1i	|- ( y e. On -> (/) = ( (/) +o (/) ) )
19	14 18	eqeq12d	|- ( y e. On -> ( ( (/) .o suc y ) = (/) <-> ( ( (/) .o y ) +o (/) ) = ( (/) +o (/) ) ) )
20	12 19	syl5ibr	|- ( y e. On -> ( ( (/) .o y ) = (/) -> ( (/) .o suc y ) = (/) ) )
21		iuneq2	|- ( A. y e. x ( (/) .o y ) = (/) -> U_ y e. x ( (/) .o y ) = U_ y e. x (/) )
22		iun0	|- U_ y e. x (/) = (/)
23	21 22	eqtrdi	|- ( A. y e. x ( (/) .o y ) = (/) -> U_ y e. x ( (/) .o y ) = (/) )
24		vex	|- x e. _V
25		omlim	|- ( ( (/) e. On /\ ( x e. _V /\ Lim x ) ) -> ( (/) .o x ) = U_ y e. x ( (/) .o y ) )
26	9 25	mpan	|- ( ( x e. _V /\ Lim x ) -> ( (/) .o x ) = U_ y e. x ( (/) .o y ) )
27	24 26	mpan	|- ( Lim x -> ( (/) .o x ) = U_ y e. x ( (/) .o y ) )
28	27	eqeq1d	|- ( Lim x -> ( ( (/) .o x ) = (/) <-> U_ y e. x ( (/) .o y ) = (/) ) )
29	23 28	syl5ibr	|- ( Lim x -> ( A. y e. x ( (/) .o y ) = (/) -> ( (/) .o x ) = (/) ) )
30	2 4 6 8 11 20 29	tfinds	|- ( A e. On -> ( (/) .o A ) = (/) )