Theorem oaomoecl

Description: The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of Schloeder p. 5. See oacl , omcl , oecl . (Contributed by RP, 18-Jan-2025)

	Ref	Expression
Assertion	oaomoecl	|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. On /\ ( A .o B ) e. On /\ ( A ^o B ) e. On ) )

Proof

Step	Hyp	Ref	Expression
1		oacl	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
2		omcl	|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
3		oecl	|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
4	1 2 3	3jca	|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. On /\ ( A .o B ) e. On /\ ( A ^o B ) e. On ) )