Metamath Proof Explorer

Theorem oef1o

Description: A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption ( F(/) ) = (/) can be discharged using fveqf1o .) (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses oef1o.f 
|- ( ph -> F : A -1-1-onto-> C )
oef1o.g 
|- ( ph -> G : B -1-1-onto-> D )
oef1o.a 
|- ( ph -> A e. ( On \ 1o ) )
oef1o.b 
|- ( ph -> B e. On )
oef1o.c 
|- ( ph -> C e. On )
oef1o.d 
|- ( ph -> D e. On )
oef1o.z 
|- ( ph -> ( F ` (/) ) = (/) )
oef1o.k 
|- K = ( y e. { x e. ( A ^m B ) | x finSupp (/) } |-> ( F o. ( y o. `' G ) ) )
oef1o.h 
|- H = ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) )
Assertion oef1o 
|- ( ph -> H : ( A ^o B ) -1-1-onto-> ( C ^o D ) )

Proof

Step Hyp Ref Expression
1 oef1o.f 
 |-  ( ph -> F : A -1-1-onto-> C )
2 oef1o.g 
 |-  ( ph -> G : B -1-1-onto-> D )
3 oef1o.a 
 |-  ( ph -> A e. ( On \ 1o ) )
4 oef1o.b 
 |-  ( ph -> B e. On )
5 oef1o.c 
 |-  ( ph -> C e. On )
6 oef1o.d 
 |-  ( ph -> D e. On )
7 oef1o.z 
 |-  ( ph -> ( F ` (/) ) = (/) )
8 oef1o.k 
 |-  K = ( y e. { x e. ( A ^m B ) | x finSupp (/) } |-> ( F o. ( y o. `' G ) ) )
9 oef1o.h 
 |-  H = ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) )
10 eqid 
 |-  dom ( C CNF D ) = dom ( C CNF D )
11 10 5 6 cantnff1o 
 |-  ( ph -> ( C CNF D ) : dom ( C CNF D ) -1-1-onto-> ( C ^o D ) )
12 eqid 
 |-  { x e. ( A ^m B ) | x finSupp (/) } = { x e. ( A ^m B ) | x finSupp (/) }
13 eqid 
 |-  { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } = { x e. ( C ^m D ) | x finSupp ( F ` (/) ) }
14 eqid 
 |-  ( F ` (/) ) = ( F ` (/) )
15 f1ocnv 
 |-  ( G : B -1-1-onto-> D -> `' G : D -1-1-onto-> B )
16 2 15 syl 
 |-  ( ph -> `' G : D -1-1-onto-> B )
17 ondif1 
 |-  ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )
18 17 simprbi 
 |-  ( A e. ( On \ 1o ) -> (/) e. A )
19 3 18 syl 
 |-  ( ph -> (/) e. A )
20 12 13 14 16 1 4 3 6 5 19 mapfien 
 |-  ( ph -> ( y e. { x e. ( A ^m B ) | x finSupp (/) } |-> ( F o. ( y o. `' G ) ) ) : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } )
21 f1oeq1 
 |-  ( K = ( y e. { x e. ( A ^m B ) | x finSupp (/) } |-> ( F o. ( y o. `' G ) ) ) -> ( K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } <-> ( y e. { x e. ( A ^m B ) | x finSupp (/) } |-> ( F o. ( y o. `' G ) ) ) : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } ) )
22 8 21 ax-mp 
 |-  ( K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } <-> ( y e. { x e. ( A ^m B ) | x finSupp (/) } |-> ( F o. ( y o. `' G ) ) ) : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } )
23 20 22 sylibr 
 |-  ( ph -> K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } )
24 eqid 
 |-  { x e. ( C ^m D ) | x finSupp (/) } = { x e. ( C ^m D ) | x finSupp (/) }
25 24 5 6 cantnfdm 
 |-  ( ph -> dom ( C CNF D ) = { x e. ( C ^m D ) | x finSupp (/) } )
26 7 breq2d 
 |-  ( ph -> ( x finSupp ( F ` (/) ) <-> x finSupp (/) ) )
27 26 rabbidv 
 |-  ( ph -> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } = { x e. ( C ^m D ) | x finSupp (/) } )
28 25 27 eqtr4d 
 |-  ( ph -> dom ( C CNF D ) = { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } )
29 28 f1oeq3d 
 |-  ( ph -> ( K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> dom ( C CNF D ) <-> K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> { x e. ( C ^m D ) | x finSupp ( F ` (/) ) } ) )
30 23 29 mpbird 
 |-  ( ph -> K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> dom ( C CNF D ) )
31 3 eldifad 
 |-  ( ph -> A e. On )
32 12 31 4 cantnfdm 
 |-  ( ph -> dom ( A CNF B ) = { x e. ( A ^m B ) | x finSupp (/) } )
33 32 f1oeq2d 
 |-  ( ph -> ( K : dom ( A CNF B ) -1-1-onto-> dom ( C CNF D ) <-> K : { x e. ( A ^m B ) | x finSupp (/) } -1-1-onto-> dom ( C CNF D ) ) )
34 30 33 mpbird 
 |-  ( ph -> K : dom ( A CNF B ) -1-1-onto-> dom ( C CNF D ) )
35 f1oco 
 |-  ( ( ( C CNF D ) : dom ( C CNF D ) -1-1-onto-> ( C ^o D ) /\ K : dom ( A CNF B ) -1-1-onto-> dom ( C CNF D ) ) -> ( ( C CNF D ) o. K ) : dom ( A CNF B ) -1-1-onto-> ( C ^o D ) )
36 11 34 35 syl2anc 
 |-  ( ph -> ( ( C CNF D ) o. K ) : dom ( A CNF B ) -1-1-onto-> ( C ^o D ) )
37 eqid 
 |-  dom ( A CNF B ) = dom ( A CNF B )
38 37 31 4 cantnff1o 
 |-  ( ph -> ( A CNF B ) : dom ( A CNF B ) -1-1-onto-> ( A ^o B ) )
39 f1ocnv 
 |-  ( ( A CNF B ) : dom ( A CNF B ) -1-1-onto-> ( A ^o B ) -> `' ( A CNF B ) : ( A ^o B ) -1-1-onto-> dom ( A CNF B ) )
40 38 39 syl 
 |-  ( ph -> `' ( A CNF B ) : ( A ^o B ) -1-1-onto-> dom ( A CNF B ) )
41 f1oco 
 |-  ( ( ( ( C CNF D ) o. K ) : dom ( A CNF B ) -1-1-onto-> ( C ^o D ) /\ `' ( A CNF B ) : ( A ^o B ) -1-1-onto-> dom ( A CNF B ) ) -> ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) ) : ( A ^o B ) -1-1-onto-> ( C ^o D ) )
42 36 40 41 syl2anc 
 |-  ( ph -> ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) ) : ( A ^o B ) -1-1-onto-> ( C ^o D ) )
43 f1oeq1 
 |-  ( H = ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) ) -> ( H : ( A ^o B ) -1-1-onto-> ( C ^o D ) <-> ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) ) : ( A ^o B ) -1-1-onto-> ( C ^o D ) ) )
44 9 43 ax-mp 
 |-  ( H : ( A ^o B ) -1-1-onto-> ( C ^o D ) <-> ( ( ( C CNF D ) o. K ) o. `' ( A CNF B ) ) : ( A ^o B ) -1-1-onto-> ( C ^o D ) )
45 42 44 sylibr 
 |-  ( ph -> H : ( A ^o B ) -1-1-onto-> ( C ^o D ) )