Metamath Proof Explorer


Theorem naddov

Description: The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddov Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) with typecode |-

Proof

Step Hyp Ref Expression
1 naddcllem Could not format ( ( 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 ) } ) ) : No typesetting found for |- ( ( 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 ) } ) ) with typecode |-
2 1 simprd Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) with typecode |-