Theorem naddov3

Description: Alternate expression for natural addition. (Contributed by Scott Fenton, 20-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		naddov	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 |-
2		unss	Could not format ( ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) <-> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ x ) : No typesetting found for |- ( ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) <-> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ x ) with typecode |-
3	2	rabbii	Could not format { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = { x e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ x } : No typesetting found for |- { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = { x e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ x } with typecode |-
4	3	inteqi	Could not format |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ x } : No typesetting found for |- |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ x } with typecode |-
5	1 4	eqtrdi	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) u. ( +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 ) ) u. ( +no " ( A X. { B } ) ) ) C_ x } ) with typecode |-