Metamath Proof Explorer

Theorem oa1cl

Description: A +o 1o is in On . (Contributed by RP, 27-Sep-2023)

Ref Expression
Assertion oa1cl 
|- ( A e. On -> ( A +o 1o ) e. On )

Proof

Step Hyp Ref Expression
1 1on 
 |-  1o e. On
2 oacl 
 |-  ( ( A e. On /\ 1o e. On ) -> ( A +o 1o ) e. On )
3 1 2 mpan2 
 |-  ( A e. On -> ( A +o 1o ) e. On )