Metamath Proof Explorer

Theorem naddcom

Description: Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddcom 
|- ( ( A e. On /\ B e. On ) -> ( A +no B ) = ( B +no A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = c -> ( a +no b ) = ( c +no b ) )
2 oveq2 
 |-  ( a = c -> ( b +no a ) = ( b +no c ) )
3 1 2 eqeq12d 
 |-  ( a = c -> ( ( a +no b ) = ( b +no a ) <-> ( c +no b ) = ( b +no c ) ) )
4 oveq2 
 |-  ( b = d -> ( c +no b ) = ( c +no d ) )
5 oveq1 
 |-  ( b = d -> ( b +no c ) = ( d +no c ) )
6 4 5 eqeq12d 
 |-  ( b = d -> ( ( c +no b ) = ( b +no c ) <-> ( c +no d ) = ( d +no c ) ) )
7 oveq1 
 |-  ( a = c -> ( a +no d ) = ( c +no d ) )
8 oveq2 
 |-  ( a = c -> ( d +no a ) = ( d +no c ) )
9 7 8 eqeq12d 
 |-  ( a = c -> ( ( a +no d ) = ( d +no a ) <-> ( c +no d ) = ( d +no c ) ) )
10 oveq1 
 |-  ( a = A -> ( a +no b ) = ( A +no b ) )
11 oveq2 
 |-  ( a = A -> ( b +no a ) = ( b +no A ) )
12 10 11 eqeq12d 
 |-  ( a = A -> ( ( a +no b ) = ( b +no a ) <-> ( A +no b ) = ( b +no A ) ) )
13 oveq2 
 |-  ( b = B -> ( A +no b ) = ( A +no B ) )
14 oveq1 
 |-  ( b = B -> ( b +no A ) = ( B +no A ) )
15 13 14 eqeq12d 
 |-  ( b = B -> ( ( A +no b ) = ( b +no A ) <-> ( A +no B ) = ( B +no A ) ) )
16 eleq1 
 |-  ( ( a +no d ) = ( d +no a ) -> ( ( a +no d ) e. x <-> ( d +no a ) e. x ) )
17 16 ralimi 
 |-  ( A. d e. b ( a +no d ) = ( d +no a ) -> A. d e. b ( ( a +no d ) e. x <-> ( d +no a ) e. x ) )
18 ralbi 
 |-  ( A. d e. b ( ( a +no d ) e. x <-> ( d +no a ) e. x ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) )
19 17 18 syl 
 |-  ( A. d e. b ( a +no d ) = ( d +no a ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) )
20 19 3ad2ant3 
 |-  ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) )
21 20 adantl 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) )
22 eleq1 
 |-  ( ( c +no b ) = ( b +no c ) -> ( ( c +no b ) e. x <-> ( b +no c ) e. x ) )
23 22 ralimi 
 |-  ( A. c e. a ( c +no b ) = ( b +no c ) -> A. c e. a ( ( c +no b ) e. x <-> ( b +no c ) e. x ) )
24 ralbi 
 |-  ( A. c e. a ( ( c +no b ) e. x <-> ( b +no c ) e. x ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) )
25 23 24 syl 
 |-  ( A. c e. a ( c +no b ) = ( b +no c ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) )
26 25 3ad2ant2 
 |-  ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) )
27 26 adantl 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) )
28 21 27 anbi12d 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) <-> ( A. d e. b ( d +no a ) e. x /\ A. c e. a ( b +no c ) e. x ) ) )
29 28 biancomd 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) <-> ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) ) )
30 29 rabbidv 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } = { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } )
31 30 inteqd 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } )
32 naddov2 
 |-  ( ( a e. On /\ b e. On ) -> ( a +no b ) = |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } )
33 32 adantr 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( a +no b ) = |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } )
34 naddov2 
 |-  ( ( b e. On /\ a e. On ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } )
35 34 ancoms 
 |-  ( ( a e. On /\ b e. On ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } )
36 35 adantr 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } )
37 31 33 36 3eqtr4d 
 |-  ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( a +no b ) = ( b +no a ) )
38 37 ex 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( a +no b ) = ( b +no a ) ) )
39 3 6 9 12 15 38 on2ind 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) = ( B +no A ) )