Metamath Proof Explorer

Theorem nmuladdel

Description: Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026)

Ref Expression
Assertion nmuladdel 
|- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = ( A .no B ) -> ( x +no ( c .no d ) ) = ( ( A .no B ) +no ( c .no d ) ) )
2 1 eleq2d 
 |-  ( x = ( A .no B ) -> ( ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) )
3 2 2ralbidv 
 |-  ( x = ( A .no B ) -> ( A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) )
4 nmulval 
 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } )
5 ssrab2 
 |-  { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } C_ On
6 nmulcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On )
7 4 6 eqeltrrd 
 |-  ( ( A e. On /\ B e. On ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On )
8 rabn0 
 |-  ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) <-> E. x e. On A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) )
9 onintrab2 
 |-  ( E. x e. On A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On )
10 8 9 bitri 
 |-  ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) <-> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On )
11 7 10 sylibr 
 |-  ( ( A e. On /\ B e. On ) -> { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) )
12 onint 
 |-  ( ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } C_ On /\ { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } )
13 5 11 12 sylancr 
 |-  ( ( A e. On /\ B e. On ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } )
14 4 13 eqeltrd 
 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } )
15 3 14 elrabrd 
 |-  ( ( A e. On /\ B e. On ) -> A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) )
16 oveq1 
 |-  ( c = C -> ( c .no B ) = ( C .no B ) )
17 16 oveq1d 
 |-  ( c = C -> ( ( c .no B ) +no ( A .no d ) ) = ( ( C .no B ) +no ( A .no d ) ) )
18 oveq1 
 |-  ( c = C -> ( c .no d ) = ( C .no d ) )
19 18 oveq2d 
 |-  ( c = C -> ( ( A .no B ) +no ( c .no d ) ) = ( ( A .no B ) +no ( C .no d ) ) )
20 17 19 eleq12d 
 |-  ( c = C -> ( ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) <-> ( ( C .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( C .no d ) ) ) )
21 oveq2 
 |-  ( d = D -> ( A .no d ) = ( A .no D ) )
22 21 oveq2d 
 |-  ( d = D -> ( ( C .no B ) +no ( A .no d ) ) = ( ( C .no B ) +no ( A .no D ) ) )
23 oveq2 
 |-  ( d = D -> ( C .no d ) = ( C .no D ) )
24 23 oveq2d 
 |-  ( d = D -> ( ( A .no B ) +no ( C .no d ) ) = ( ( A .no B ) +no ( C .no D ) ) )
25 22 24 eleq12d 
 |-  ( d = D -> ( ( ( C .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( C .no d ) ) <-> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) )
26 20 25 rspc2va 
 |-  ( ( ( C e. A /\ D e. B ) /\ A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) )
27 26 ancoms 
 |-  ( ( A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) )
28 15 27 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) )