hashfacen

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

		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		f1of	$⊢ f : A \underset{1-1 onto}{⟶} C \to f : A ⟶ C$
5		f1odm	$⊢ h : C \underset{1-1 onto}{⟶} D \to dom h = C$
6		vex	$⊢ h \in V$
7	6	dmex	$⊢ dom h \in V$
8	5 7	eqeltrrdi	$⊢ h : C \underset{1-1 onto}{⟶} D \to C \in V$
9		f1odm	$⊢ g : A \underset{1-1 onto}{⟶} B \to dom g = A$
10		vex	$⊢ g \in V$
11	10	dmex	$⊢ dom g \in V$
12	9 11	eqeltrrdi	$⊢ g : A \underset{1-1 onto}{⟶} B \to A \in V$
13		elmapg	$⊢ (C \in V \land A \in V) \to (f \in (C^{A}) \leftrightarrow f : A ⟶ C)$
14	8 12 13	syl2anr	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (f \in (C^{A}) \leftrightarrow f : A ⟶ C)$
15	4 14	syl5ibr	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (f : A \underset{1-1 onto}{⟶} C \to f \in (C^{A}))$
16	15	abssdv	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \subseteq C^{A}$
17		ovex	$⊢ C^{A} \in V$
18	17	ssex	$⊢ \{f \| f : A \underset{1-1 onto}{⟶} C\} \subseteq C^{A} \to \{f \| f : A \underset{1-1 onto}{⟶} C\} \in V$
19	16 18	syl	$⊢ (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$
20		f1of	$⊢ f : B \underset{1-1 onto}{⟶} D \to f : B ⟶ D$
21		f1ofo	$⊢ h : C \underset{1-1 onto}{⟶} D \to h : C \underset{onto}{⟶} D$
22		forn	$⊢ h : C \underset{onto}{⟶} D \to ran h = D$
23	21 22	syl	$⊢ h : C \underset{1-1 onto}{⟶} D \to ran h = D$
24	6	rnex	$⊢ ran h \in V$
25	23 24	eqeltrrdi	$⊢ h : C \underset{1-1 onto}{⟶} D \to D \in V$
26		f1ofo	$⊢ g : A \underset{1-1 onto}{⟶} B \to g : A \underset{onto}{⟶} B$
27		forn	$⊢ g : A \underset{onto}{⟶} B \to ran g = B$
28	26 27	syl	$⊢ g : A \underset{1-1 onto}{⟶} B \to ran g = B$
29	10	rnex	$⊢ ran g \in V$
30	28 29	eqeltrrdi	$⊢ g : A \underset{1-1 onto}{⟶} B \to B \in V$
31		elmapg	$⊢ (D \in V \land B \in V) \to (f \in (D^{B}) \leftrightarrow f : B ⟶ D)$
32	25 30 31	syl2anr	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (f \in (D^{B}) \leftrightarrow f : B ⟶ D)$
33	20 32	syl5ibr	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to (f : B \underset{1-1 onto}{⟶} D \to f \in (D^{B}))$
34	33	abssdv	$⊢ (g : A \underset{1-1 onto}{⟶} B \land h : C \underset{1-1 onto}{⟶} D) \to \{f \| f : B \underset{1-1 onto}{⟶} D\} \subseteq D^{B}$
35		ovex	$⊢ D^{B} \in V$
36	35	ssex	$⊢ \{f \| f : B \underset{1-1 onto}{⟶} D\} \subseteq D^{B} \to \{f \| f : B \underset{1-1 onto}{⟶} D\} \in V$
37	34 36	syl	$⊢ (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$
38		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$
39	38	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$
40		f1ocnv	$⊢ g : A \underset{1-1 onto}{⟶} B \to g^{-1} : B \underset{1-1 onto}{⟶} A$
41	40	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$
42		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$
43	39 41 42	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$
44	43	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)$
45		vex	$⊢ x \in V$
46		f1oeq1	$⊢ f = x \to (f : A \underset{1-1 onto}{⟶} C \leftrightarrow x : A \underset{1-1 onto}{⟶} C)$
47	45 46	elab	$⊢ x \in \{f \| f : A \underset{1-1 onto}{⟶} C\} \leftrightarrow x : A \underset{1-1 onto}{⟶} C$
48	6 45	coex	$⊢ h \circ x \in V$
49	10	cnvex	$⊢ g^{-1} \in V$
50	48 49	coex	$⊢ (h \circ x) \circ g^{-1} \in V$
51		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)$
52	50 51	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$
53	44 47 52	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\})$
54		f1ocnv	$⊢ h : C \underset{1-1 onto}{⟶} D \to h^{-1} : D \underset{1-1 onto}{⟶} C$
55	54	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$
56		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$
57	56	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$
58	57	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$
59		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$
60	55 58 59	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$
61	60	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)$
62		vex	$⊢ y \in V$
63		f1oeq1	$⊢ f = y \to (f : B \underset{1-1 onto}{⟶} D \leftrightarrow y : B \underset{1-1 onto}{⟶} D)$
64	62 63	elab	$⊢ y \in \{f \| f : B \underset{1-1 onto}{⟶} D\} \leftrightarrow y : B \underset{1-1 onto}{⟶} D$
65	6	cnvex	$⊢ h^{-1} \in V$
66	62 10	coex	$⊢ y \circ g \in V$
67	65 66	coex	$⊢ h^{-1} \circ (y \circ g) \in V$
68		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)$
69	67 68	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$
70	61 64 69	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\})$
71	47 64	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)$
72		coass	$⊢ ((h \circ x) \circ g^{-1}) \circ g = (h \circ x) \circ (g^{-1} \circ g)$
73		f1ococnv1	$⊢ g : A \underset{1-1 onto}{⟶} B \to g^{-1} \circ g = {I ↾}_{A}$
74	73	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}$
75	74	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})$
76	39	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$
77		f1of	$⊢ (h \circ x) : A \underset{1-1 onto}{⟶} D \to (h \circ x) : A ⟶ D$
78		fcoi1	$⊢ (h \circ x) : A ⟶ D \to (h \circ x) \circ ({I ↾}_{A}) = h \circ x$
79	76 77 78	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$
80	75 79	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$
81	72 80	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$
82		coass	$⊢ (h \circ h^{-1}) \circ (y \circ g) = h \circ (h^{-1} \circ (y \circ g))$
83		f1ococnv2	$⊢ h : C \underset{1-1 onto}{⟶} D \to h \circ h^{-1} = {I ↾}_{D}$
84	83	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}$
85	84	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)$
86	58	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$
87		f1of	$⊢ (y \circ g) : A \underset{1-1 onto}{⟶} D \to (y \circ g) : A ⟶ D$
88		fcoi2	$⊢ (y \circ g) : A ⟶ D \to ({I ↾}_{D}) \circ (y \circ g) = y \circ g$
89	86 87 88	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$
90	85 89	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$
91	82 90	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$
92	81 91	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)$
93		eqcom	$⊢ ((h \circ x) \circ g^{-1}) \circ g = y \circ g \leftrightarrow y \circ g = ((h \circ x) \circ g^{-1}) \circ g$
94	92 93	syl6bb	$⊢ ((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)$
95		f1of1	$⊢ h : C \underset{1-1 onto}{⟶} D \to h : C \underset{1-1}{⟶} D$
96	95	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$
97		f1of	$⊢ x : A \underset{1-1 onto}{⟶} C \to x : A ⟶ C$
98	97	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$
99	60	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$
100		f1of	$⊢ (h^{-1} \circ (y \circ g)) : A \underset{1-1 onto}{⟶} C \to (h^{-1} \circ (y \circ g)) : A ⟶ C$
101	99 100	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$
102		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))$
103	96 98 101 102	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))$
104	26	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$
105		f1ofn	$⊢ y : B \underset{1-1 onto}{⟶} D \to y Fn B$
106	105	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$
107	43	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$
108		f1ofn	$⊢ ((h \circ x) \circ g^{-1}) : B \underset{1-1 onto}{⟶} D \to ((h \circ x) \circ g^{-1}) Fn B$
109	107 108	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$
110		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})$
111	104 106 109 110	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})$
112	94 103 111	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})$
113	112	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}))$
114	71 113	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}))$
115	19 37 53 70 114	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\}$
116	115	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\}$
117	3 116	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\}$
118	1 2 117	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