Description: Closure law for natural addition. (Contributed by Scott Fenton, 26-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | naddcl | |- ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | naddcllem | |- ( ( A e. On /\ B e. On ) -> ( ( A +no B ) e. On /\ ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) ) |
|
2 | 1 | simpld | |- ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On ) |