Theorem naddov4

Description: Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		naddov2	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } ) with typecode |-
2		inrab	Could not format ( { x e. On | A. b e. B ( A +no b ) e. x } i^i { x e. On | A. a e. A ( a +no B ) e. x } ) = { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } : No typesetting found for |- ( { x e. On | A. b e. B ( A +no b ) e. x } i^i { x e. On | A. a e. A ( a +no B ) e. x } ) = { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } with typecode |-
3		incom	Could not format ( { x e. On | A. b e. B ( A +no b ) e. x } i^i { x e. On | A. a e. A ( a +no B ) e. x } ) = ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) : No typesetting found for |- ( { x e. On | A. b e. B ( A +no b ) e. x } i^i { x e. On | A. a e. A ( a +no B ) e. x } ) = ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) with typecode |-
4	2 3	eqtr3i	Could not format { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } = ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) : No typesetting found for |- { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } = ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) with typecode |-
5	4	inteqi	Could not format |^| { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } = |^| ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) : No typesetting found for |- |^| { x e. On | ( A. b e. B ( A +no b ) e. x /\ A. a e. A ( a +no B ) e. x ) } = |^| ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) with typecode |-
6	1 5	eqtrdi	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| ( { x e. On | A. a e. A ( a +no B ) e. x } i^i { x e. On | A. b e. B ( A +no b ) e. x } ) ) with typecode |-