Metamath Proof Explorer

Theorem oenass

Description: Ordinal exponentiation is not associative. Remark 4.6 of Schloeder p. 14. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion oenass 
|- E. a e. On E. b e. On E. c e. On -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c )

Proof

Step Hyp Ref Expression
1 oenassex 
 |-  -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) )
2 2on 
 |-  2o e. On
3 0elon 
 |-  (/) e. On
4 oveq2 
 |-  ( c = (/) -> ( 2o ^o c ) = ( 2o ^o (/) ) )
5 4 oveq2d 
 |-  ( c = (/) -> ( 2o ^o ( 2o ^o c ) ) = ( 2o ^o ( 2o ^o (/) ) ) )
6 oveq2 
 |-  ( c = (/) -> ( ( 2o ^o 2o ) ^o c ) = ( ( 2o ^o 2o ) ^o (/) ) )
7 5 6 eqeq12d 
 |-  ( c = (/) -> ( ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) <-> ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) ) )
8 7 notbid 
 |-  ( c = (/) -> ( -. ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) <-> -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) ) )
9 8 rspcev 
 |-  ( ( (/) e. On /\ -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) ) -> E. c e. On -. ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) )
10 3 9 mpan 
 |-  ( -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) -> E. c e. On -. ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) )
11 oveq1 
 |-  ( b = 2o -> ( b ^o c ) = ( 2o ^o c ) )
12 11 oveq2d 
 |-  ( b = 2o -> ( 2o ^o ( b ^o c ) ) = ( 2o ^o ( 2o ^o c ) ) )
13 oveq2 
 |-  ( b = 2o -> ( 2o ^o b ) = ( 2o ^o 2o ) )
14 13 oveq1d 
 |-  ( b = 2o -> ( ( 2o ^o b ) ^o c ) = ( ( 2o ^o 2o ) ^o c ) )
15 12 14 eqeq12d 
 |-  ( b = 2o -> ( ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) <-> ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) ) )
16 15 notbid 
 |-  ( b = 2o -> ( -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) <-> -. ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) ) )
17 16 rexbidv 
 |-  ( b = 2o -> ( E. c e. On -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) <-> E. c e. On -. ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) ) )
18 17 rspcev 
 |-  ( ( 2o e. On /\ E. c e. On -. ( 2o ^o ( 2o ^o c ) ) = ( ( 2o ^o 2o ) ^o c ) ) -> E. b e. On E. c e. On -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) )
19 2 10 18 sylancr 
 |-  ( -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) -> E. b e. On E. c e. On -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) )
20 oveq1 
 |-  ( a = 2o -> ( a ^o ( b ^o c ) ) = ( 2o ^o ( b ^o c ) ) )
21 oveq1 
 |-  ( a = 2o -> ( a ^o b ) = ( 2o ^o b ) )
22 21 oveq1d 
 |-  ( a = 2o -> ( ( a ^o b ) ^o c ) = ( ( 2o ^o b ) ^o c ) )
23 20 22 eqeq12d 
 |-  ( a = 2o -> ( ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c ) <-> ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) ) )
24 23 notbid 
 |-  ( a = 2o -> ( -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c ) <-> -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) ) )
25 24 rexbidv 
 |-  ( a = 2o -> ( E. c e. On -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c ) <-> E. c e. On -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) ) )
26 25 rexbidv 
 |-  ( a = 2o -> ( E. b e. On E. c e. On -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c ) <-> E. b e. On E. c e. On -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) ) )
27 26 rspcev 
 |-  ( ( 2o e. On /\ E. b e. On E. c e. On -. ( 2o ^o ( b ^o c ) ) = ( ( 2o ^o b ) ^o c ) ) -> E. a e. On E. b e. On E. c e. On -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c ) )
28 2 19 27 sylancr 
 |-  ( -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) -> E. a e. On E. b e. On E. c e. On -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c ) )
29 1 28 ax-mp 
 |-  E. a e. On E. b e. On E. c e. On -. ( a ^o ( b ^o c ) ) = ( ( a ^o b ) ^o c )