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	$⊢ φ \to F : A \underset{1-1 onto}{⟶} C$
	oef1o.g	$⊢ φ \to G : B \underset{1-1 onto}{⟶} D$
	oef1o.a	$⊢ φ \to A \in (On ∖ 1_{𝑜})$
	oef1o.b	$⊢ φ \to B \in On$
	oef1o.c	$⊢ φ \to C \in On$
	oef1o.d	$⊢ φ \to D \in On$
	oef1o.z	$⊢ φ \to F (\emptyset) = \emptyset$
	oef1o.k	$⊢ K = (y \in \{x \in (A^{B}) \| {finSupp}_{\emptyset} (x)\} ⟼ F \circ (y \circ G^{-1}))$
	oef1o.h	$⊢ H = ((C CNF D) \circ K) \circ {(A CNF B)}^{-1}$
Assertion	oef1o	$⊢ φ \to H : A ↑_{𝑜} B \underset{1-1 onto}{⟶} C ↑_{𝑜} D$

Proof

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

Metamath Proof Explorer

Theorem oef1o

Proof