hashfacen

Description: The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015) (Proof shortened by AV, 7-Aug-2024)

		Ref	Expression
	Assertion	hashfacen	$⊢ (A \approx B \land C \approx D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \approx \{f \| f : B \underset{1-1 onto}{⟶} D\}$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx B \leftrightarrow \exists g g : A \underset{1-1 onto}{⟶} B$
2		bren	$⊢ C \approx D \leftrightarrow \exists h h : C \underset{1-1 onto}{⟶} D$
3		exdistrv	$⊢ \exists g \exists h (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \leftrightarrow (\exists g g : A \underset{1-1 onto}{⟶} B \land \exists h h : C \underset{1-1 onto}{⟶} D)$
4		f1osetex	$⊢ \{f \| f : A \underset{1-1 onto}{⟶} C\} \in V$
5	4	a1i	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \in V$
6		f1osetex	$⊢ \{f \| f : B \underset{1-1 onto}{⟶} D\} \in V$
7	6	a1i	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : B \underset{1-1 onto}{⟶} D\} \in V$
8		f1oco	$⊢ (h : C \underset{1-1 onto}{⟶} D \land x : A \underset{1-1 onto}{⟶} C) \to (h \circ x) : A \underset{1-1 onto}{⟶} D$
9	8	adantll	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land x : A \underset{1-1 onto}{⟶} C) \to (h \circ x) : A \underset{1-1 onto}{⟶} D$
10		f1ocnv	$⊢ g : A \underset{1-1 onto}{⟶} B \to g^{-1} : B \underset{1-1 onto}{⟶} A$
11	10	ad2antrr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land x : A \underset{1-1 onto}{⟶} C) \to g^{-1} : B \underset{1-1 onto}{⟶} A$
12		f1oco	$⊢ ((h \circ x) : A \underset{1-1 onto}{⟶} D \land g^{-1} : B \underset{1-1 onto}{⟶} A) \to ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D$
13	9 11 12	syl2anc	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land x : A \underset{1-1 onto}{⟶} C) \to ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D$
14	13	ex	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (x : A \underset{1-1 onto}{⟶} C \to ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D)$
15		vex	$⊢ x \in V$
16		f1oeq1	$⊢ f = x \to (f : A \underset{1-1 onto}{⟶} C \leftrightarrow x : A \underset{1-1 onto}{⟶} C)$
17	15 16	elab	$⊢ x \in \{f \| f : A \underset{1-1 onto}{⟶} C\} \leftrightarrow x : A \underset{1-1 onto}{⟶} C$
18		vex	$⊢ h \in V$
19	18 15	coex	$⊢ h \circ x \in V$
20		vex	$⊢ g \in V$
21	20	cnvex	$⊢ g^{-1} \in V$
22	19 21	coex	$⊢ (h \circ x) \circ g^{-1} \in V$
23		f1oeq1	$⊢ f = (h \circ x) \circ g^{-1} \to (f : B \underset{1-1 onto}{⟶} D \leftrightarrow ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D)$
24	22 23	elab	$⊢ (h \circ x) \circ g^{-1} \in \{f \| f : B \underset{1-1 onto}{⟶} D\} \leftrightarrow ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D$
25	14 17 24	3imtr4g	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (x \in \{f \| f : A \underset{1-1 onto}{⟶} C\} \to (h \circ x) \circ g^{-1} \in \{f \| f : B \underset{1-1 onto}{⟶} D\})$
26		f1ocnv	$⊢ h : C \underset{1-1 onto}{⟶} D \to h^{-1} : D \underset{1-1 onto}{⟶} C$
27	26	ad2antlr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land y : B \underset{1-1 onto}{⟶} D) \to h^{-1} : D \underset{1-1 onto}{⟶} C$
28		f1oco	$⊢ (y : B \underset{1-1 onto}{⟶} D \land g : A \underset{1-1 onto}{⟶} B) \to (y \circ g) : A \underset{1-1 onto}{⟶} D$
29	28	ancoms	$⊢ (g : A \underset{1-1 onto}{⟶} B \land y : B \underset{1-1 onto}{⟶} D) \to (y \circ g) : A \underset{1-1 onto}{⟶} D$
30	29	adantlr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land y : B \underset{1-1 onto}{⟶} D) \to (y \circ g) : A \underset{1-1 onto}{⟶} D$
31		f1oco	$⊢ (h^{-1} : D \underset{1-1 onto}{⟶} C \land (y \circ g) : A \underset{1-1 onto}{⟶} D) \to (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C$
32	27 30 31	syl2anc	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land y : B \underset{1-1 onto}{⟶} D) \to (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C$
33	32	ex	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (y : B \underset{1-1 onto}{⟶} D \to (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C)$
34		vex	$⊢ y \in V$
35		f1oeq1	$⊢ f = y \to (f : B \underset{1-1 onto}{⟶} D \leftrightarrow y : B \underset{1-1 onto}{⟶} D)$
36	34 35	elab	$⊢ y \in \{f \| f : B \underset{1-1 onto}{⟶} D\} \leftrightarrow y : B \underset{1-1 onto}{⟶} D$
37	18	cnvex	$⊢ h^{-1} \in V$
38	34 20	coex	$⊢ y \circ g \in V$
39	37 38	coex	$⊢ h^{-1} \circ (y \circ g) \in V$
40		f1oeq1	$⊢ f = h^{-1} \circ (y \circ g) \to (f : A \underset{1-1 onto}{⟶} C \leftrightarrow (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C)$
41	39 40	elab	$⊢ h^{-1} \circ (y \circ g) \in \{f \| f : A \underset{1-1 onto}{⟶} C\} \leftrightarrow (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C$
42	33 36 41	3imtr4g	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (y \in \{f \| f : B \underset{1-1 onto}{⟶} D\} \to h^{-1} \circ (y \circ g) \in \{f \| f : A \underset{1-1 onto}{⟶} C\})$
43	17 36	anbi12i	$⊢ (x \in \{f \| f : A \underset{1-1 onto}{⟶} C\} \land y \in \{f \| f : B \underset{1-1 onto}{⟶} D\}) \leftrightarrow (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)$
44		coass	$⊢ ((h \circ x) \circ g^{-1}) \circ g = (h \circ x) \circ (g^{-1} \circ g)$
45		f1ococnv1	$⊢ g : A \underset{1-1 onto}{⟶} B \to g^{-1} \circ g = {I ↾}_{A}$
46	45	ad2antrr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to g^{-1} \circ g = {I ↾}_{A}$
47	46	coeq2d	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x) \circ (g^{-1} \circ g) = (h \circ x) \circ ({I ↾}_{A})$
48	9	adantrr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x) : A \underset{1-1 onto}{⟶} D$
49		f1of	$⊢ (h \circ x) : A \underset{1-1 onto}{⟶} D \to (h \circ x) : A ⟶ D$
50		fcoi1	$⊢ (h \circ x) : A ⟶ D \to (h \circ x) \circ ({I ↾}_{A}) = h \circ x$
51	48 49 50	3syl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x) \circ ({I ↾}_{A}) = h \circ x$
52	47 51	eqtrd	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x) \circ (g^{-1} \circ g) = h \circ x$
53	44 52	syl5req	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to h \circ x = ((h \circ x) \circ g^{-1}) \circ g$
54		coass	$⊢ (h \circ h^{-1}) \circ (y \circ g) = h \circ (h^{-1} \circ (y \circ g))$
55		f1ococnv2	$⊢ h : C \underset{1-1 onto}{⟶} D \to h \circ h^{-1} = {I ↾}_{D}$
56	55	ad2antlr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to h \circ h^{-1} = {I ↾}_{D}$
57	56	coeq1d	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ h^{-1}) \circ (y \circ g) = ({I ↾}_{D}) \circ (y \circ g)$
58	30	adantrl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (y \circ g) : A \underset{1-1 onto}{⟶} D$
59		f1of	$⊢ (y \circ g) : A \underset{1-1 onto}{⟶} D \to (y \circ g) : A ⟶ D$
60		fcoi2	$⊢ (y \circ g) : A ⟶ D \to ({I ↾}_{D}) \circ (y \circ g) = y \circ g$
61	58 59 60	3syl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to ({I ↾}_{D}) \circ (y \circ g) = y \circ g$
62	57 61	eqtrd	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ h^{-1}) \circ (y \circ g) = y \circ g$
63	54 62	syl5eqr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to h \circ (h^{-1} \circ (y \circ g)) = y \circ g$
64	53 63	eqeq12d	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x = h \circ (h^{-1} \circ (y \circ g)) \leftrightarrow ((h \circ x) \circ g^{-1}) \circ g = y \circ g)$
65		eqcom	$⊢ ((h \circ x) \circ g^{-1}) \circ g = y \circ g \leftrightarrow y \circ g = ((h \circ x) \circ g^{-1}) \circ g$
66	64 65	bitrdi	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x = h \circ (h^{-1} \circ (y \circ g)) \leftrightarrow y \circ g = ((h \circ x) \circ g^{-1}) \circ g)$
67		f1of1	$⊢ h : C \underset{1-1 onto}{⟶} D \to h : C \underset{1-1}{⟶} D$
68	67	ad2antlr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to h : C \underset{1-1}{⟶} D$
69		f1of	$⊢ x : A \underset{1-1 onto}{⟶} C \to x : A ⟶ C$
70	69	ad2antrl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to x : A ⟶ C$
71	32	adantrl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C$
72		f1of	$⊢ (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C \to (h^{-1} \circ (y \circ g)) : A ⟶ C$
73	71 72	syl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h^{-1} \circ (y \circ g)) : A ⟶ C$
74		cocan1	$⊢ (h : C \underset{1-1}{⟶} D \land x : A ⟶ C \land (h^{-1} \circ (y \circ g)) : A ⟶ C) \to (h \circ x = h \circ (h^{-1} \circ (y \circ g)) \leftrightarrow x = h^{-1} \circ (y \circ g))$
75	68 70 73 74	syl3anc	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (h \circ x = h \circ (h^{-1} \circ (y \circ g)) \leftrightarrow x = h^{-1} \circ (y \circ g))$
76		f1ofo	$⊢ g : A \underset{1-1 onto}{⟶} B \to g : A \underset{onto}{⟶} B$
77	76	ad2antrr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to g : A \underset{onto}{⟶} B$
78		f1ofn	$⊢ y : B \underset{1-1 onto}{⟶} D \to y Fn B$
79	78	ad2antll	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to y Fn B$
80	13	adantrr	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D$
81		f1ofn	$⊢ ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D \to ((h \circ x) \circ g^{-1}) Fn B$
82	80 81	syl	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to ((h \circ x) \circ g^{-1}) Fn B$
83		cocan2	$⊢ (g : A \underset{onto}{⟶} B \land y Fn B \land ((h \circ x) \circ g^{-1}) Fn B) \to (y \circ g = ((h \circ x) \circ g^{-1}) \circ g \leftrightarrow y = (h \circ x) \circ g^{-1})$
84	77 79 82 83	syl3anc	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (y \circ g = ((h \circ x) \circ g^{-1}) \circ g \leftrightarrow y = (h \circ x) \circ g^{-1})$
85	66 75 84	3bitr3d	$⊢ ((g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \land (x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D)) \to (x = h^{-1} \circ (y \circ g) \leftrightarrow y = (h \circ x) \circ g^{-1})$
86	85	ex	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to ((x : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to (x = h^{-1} \circ (y \circ g) \leftrightarrow y = (h \circ x) \circ g^{-1}))$
87	43 86	syl5bi	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to ((x \in \{f \| f : A \underset{1-1 onto}{⟶} C\} \land y \in \{f \| f : B \underset{1-1 onto}{⟶} D\}) \to (x = h^{-1} \circ (y \circ g) \leftrightarrow y = (h \circ x) \circ g^{-1}))$
88	5 7 25 42 87	en3d	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \approx \{f \| f : B \underset{1-1 onto}{⟶} D\}$
89	88	exlimivv	$⊢ \exists g \exists h (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \approx \{f \| f : B \underset{1-1 onto}{⟶} D\}$
90	3 89	sylbir	$⊢ (\exists g g : A \underset{1-1 onto}{⟶} B \land \exists h h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \approx \{f \| f : B \underset{1-1 onto}{⟶} D\}$
91	1 2 90	syl2anb	$⊢ (A \approx B \land C \approx D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \approx \{f \| f : B \underset{1-1 onto}{⟶} D\}$

Metamath Proof Explorer

Theorem hashfacen

Proof