Metamath Proof Explorer

Theorem naddov

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

		Ref	Expression
	Assertion	naddov	\|- ( ( A e. On /\ B e. On ) -> ( A +no B ) = \|^\| { x e. On \| ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } )

Proof

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	simprd	\|- ( ( A e. On /\ B e. On ) -> ( A +no B ) = \|^\| { x e. On \| ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } )

Step

Hyp

Ref

Expression

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 ) } ) )

simprd

 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } )