Metamath Proof Explorer

Theorem naddov4

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

Ref Expression
Assertion naddov4 
|- ( ( 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 } ) )

Proof

Step Hyp Ref Expression
1 naddov2 
 |-  ( ( 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 ) } )
2 inrab 
 |-  ( { 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 ) }
3 incom 
 |-  ( { 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 } )
4 2 3 eqtr3i 
 |-  { 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 } )
5 4 inteqi 
 |-  |^| { 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 } )
6 1 5 eqtrdi 
 |-  ( ( 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 } ) )