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 ∖ 1_o ) )
	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 ∖ 1_o ) )
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 ∖ 1_o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
18	17	simprbi	⊢ ( 𝐴 ∈ ( On ∖ 1_o ) → ∅ ∈ 𝐴 )
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 𝐷 ) )

Metamath Proof Explorer

Theorem oef1o

Proof