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 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
oef1o.g ⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
oef1o.a ⊢ ( 𝜑 → 𝐴 ∈ ( On ∖ 1o ) )
oef1o.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oef1o.c ⊢ ( 𝜑 → 𝐶 ∈ On )
oef1o.d ⊢ ( 𝜑 → 𝐷 ∈ On )
oef1o.z ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
oef1o.k ⊢ 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ 𝐺 ) ) )
oef1o.h ⊢ 𝐻 = ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) )
Assertion oef1o ( 𝜑 → 𝐻 : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )

Proof

Step Hyp Ref Expression
1 oef1o.f ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
2 oef1o.g ⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
3 oef1o.a ⊢ ( 𝜑 → 𝐴 ∈ ( On ∖ 1o ) )
4 oef1o.b ⊢ ( 𝜑 → 𝐵 ∈ On )
5 oef1o.c ⊢ ( 𝜑 → 𝐶 ∈ On )
6 oef1o.d ⊢ ( 𝜑 → 𝐷 ∈ On )
7 oef1o.z ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
8 oef1o.k ⊢ 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ 𝐺 ) ) )
9 oef1o.h ⊢ 𝐻 = ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) )
10 eqid ⊢ dom ( 𝐶 CNF 𝐷 ) = dom ( 𝐶 CNF 𝐷 )
11 10 5 6 cantnff1o ⊢ ( 𝜑 → ( 𝐶 CNF 𝐷 ) : dom ( 𝐶 CNF 𝐷 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )
12 eqid ⊢ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } = { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ }
13 eqid ⊢ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } = { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) }
14 eqid ⊢ ( 𝐹 ‘ ∅ ) = ( 𝐹 ‘ ∅ )
15 f1ocnv ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
16 2 15 syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
17 ondif1 ⊢ ( 𝐴 ∈ ( On ∖ 1o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
18 17 simprbi ⊢ ( 𝐴 ∈ ( On ∖ 1o ) → ∅ ∈ 𝐴 )
19 3 18 syl ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
20 12 13 14 16 1 4 3 6 5 19 mapfien ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ 𝐺 ) ) ) : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } )
21 f1oeq1 ⊢ ( 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ 𝐺 ) ) ) → ( 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } ↔ ( 𝑦 ∈ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ 𝐺 ) ) ) : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } ) )
22 8 21 ax-mp ⊢ ( 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } ↔ ( 𝑦 ∈ { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ 𝐺 ) ) ) : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } )
23 20 22 sylibr ⊢ ( 𝜑 → 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } )
24 eqid ⊢ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ∅ } = { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ∅ }
25 24 5 6 cantnfdm ⊢ ( 𝜑 → dom ( 𝐶 CNF 𝐷 ) = { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ∅ } )
26 7 breq2d ⊢ ( 𝜑 → ( 𝑥 finSupp ( 𝐹 ‘ ∅ ) ↔ 𝑥 finSupp ∅ ) )
27 26 rabbidv ⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } = { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ∅ } )
28 25 27 eqtr4d ⊢ ( 𝜑 → dom ( 𝐶 CNF 𝐷 ) = { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } )
29 28 f1oeq3d ⊢ ( 𝜑 → ( 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ dom ( 𝐶 CNF 𝐷 ) ↔ 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ { 𝑥 ∈ ( 𝐶 ↑m 𝐷 ) ∣ 𝑥 finSupp ( 𝐹 ‘ ∅ ) } ) )
30 23 29 mpbird ⊢ ( 𝜑 → 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ dom ( 𝐶 CNF 𝐷 ) )
31 3 eldifad ⊢ ( 𝜑 → 𝐴 ∈ On )
32 12 31 4 cantnfdm ⊢ ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } )
33 32 f1oeq2d ⊢ ( 𝜑 → ( 𝐾 : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ dom ( 𝐶 CNF 𝐷 ) ↔ 𝐾 : { 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑥 finSupp ∅ } –1-1-onto→ dom ( 𝐶 CNF 𝐷 ) ) )
34 30 33 mpbird ⊢ ( 𝜑 → 𝐾 : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ dom ( 𝐶 CNF 𝐷 ) )
35 f1oco ⊢ ( ( ( 𝐶 CNF 𝐷 ) : dom ( 𝐶 CNF 𝐷 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) ∧ 𝐾 : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ dom ( 𝐶 CNF 𝐷 ) ) → ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )
36 11 34 35 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )
37 eqid ⊢ dom ( 𝐴 CNF 𝐵 ) = dom ( 𝐴 CNF 𝐵 )
38 37 31 4 cantnff1o ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ ( 𝐴 ↑o 𝐵 ) )
39 f1ocnv ⊢ ( ( 𝐴 CNF 𝐵 ) : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ ( 𝐴 ↑o 𝐵 ) → ◡ ( 𝐴 CNF 𝐵 ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ dom ( 𝐴 CNF 𝐵 ) )
40 38 39 syl ⊢ ( 𝜑 → ◡ ( 𝐴 CNF 𝐵 ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ dom ( 𝐴 CNF 𝐵 ) )
41 f1oco ⊢ ( ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) : dom ( 𝐴 CNF 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ dom ( 𝐴 CNF 𝐵 ) ) → ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )
42 36 40 41 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )
43 f1oeq1 ⊢ ( 𝐻 = ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) ) → ( 𝐻 : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) ↔ ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) ) )
44 9 43 ax-mp ⊢ ( 𝐻 : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) ↔ ( ( ( 𝐶 CNF 𝐷 ) ∘ 𝐾 ) ∘ ◡ ( 𝐴 CNF 𝐵 ) ) : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )
45 42 44 sylibr ⊢ ( 𝜑 → 𝐻 : ( 𝐴 ↑o 𝐵 ) –1-1-onto→ ( 𝐶 ↑o 𝐷 ) )