Theorem hashfacen 13238

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

Assertion

Ref	Expression
hashfacen	⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝐶,𝑓   𝐷,𝑓

Proof of Theorem hashfacen

Dummy variables 𝑔 ℎ 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bren 7964	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑔 𝑔:𝐴–1-1-onto→𝐵)
2		bren 7964	. 2 ⊢ (𝐶 ≈ 𝐷 ↔ ∃ℎ ℎ:𝐶–1-1-onto→𝐷)
3		eeanv 2182	. . 3 ⊢ (∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ↔ (∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷))
4		f1of 6137	. . . . . . . 8 ⊢ (𝑓:𝐴–1-1-onto→𝐶 → 𝑓:𝐴⟶𝐶)
5		f1odm 6141	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → dom ℎ = 𝐶)
6		vex 3203	. . . . . . . . . . 11 ⊢ ℎ ∈ V
7	6	dmex 7099	. . . . . . . . . 10 ⊢ dom ℎ ∈ V
8	5, 7	syl6eqelr 2710	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐶 ∈ V)
9		f1odm 6141	. . . . . . . . . 10 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → dom 𝑔 = 𝐴)
10		vex 3203	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
11	10	dmex 7099	. . . . . . . . . 10 ⊢ dom 𝑔 ∈ V
12	9, 11	syl6eqelr 2710	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
13		elmapg 7870	. . . . . . . . 9 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝑓 ∈ (𝐶 ↑𝑚 𝐴) ↔ 𝑓:𝐴⟶𝐶))
14	8, 12, 13	syl2anr 495	. . . . . . . 8 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐶 ↑𝑚 𝐴) ↔ 𝑓:𝐴⟶𝐶))
15	4, 14	syl5ibr 236	. . . . . . 7 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐴–1-1-onto→𝐶 → 𝑓 ∈ (𝐶 ↑𝑚 𝐴)))
16	15	abssdv 3676	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑𝑚 𝐴))
17		ovex 6678	. . . . . . 7 ⊢ (𝐶 ↑𝑚 𝐴) ∈ V
18	17	ssex 4802	. . . . . 6 ⊢ ({𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑𝑚 𝐴) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V)
19	16, 18	syl 17	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V)
20		f1of 6137	. . . . . . . 8 ⊢ (𝑓:𝐵–1-1-onto→𝐷 → 𝑓:𝐵⟶𝐷)
21		f1ofo 6144	. . . . . . . . . . 11 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–onto→𝐷)
22		forn 6118	. . . . . . . . . . 11 ⊢ (ℎ:𝐶–onto→𝐷 → ran ℎ = 𝐷)
23	21, 22	syl 17	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ran ℎ = 𝐷)
24	6	rnex 7100	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
25	23, 24	syl6eqelr 2710	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐷 ∈ V)
26		f1ofo 6144	. . . . . . . . . . 11 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝑔:𝐴–onto→𝐵)
27		forn 6118	. . . . . . . . . . 11 ⊢ (𝑔:𝐴–onto→𝐵 → ran 𝑔 = 𝐵)
28	26, 27	syl 17	. . . . . . . . . 10 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → ran 𝑔 = 𝐵)
29	10	rnex 7100	. . . . . . . . . 10 ⊢ ran 𝑔 ∈ V
30	28, 29	syl6eqelr 2710	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
31		elmapg 7870	. . . . . . . . 9 ⊢ ((𝐷 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ (𝐷 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝐷))
32	25, 30, 31	syl2anr 495	. . . . . . . 8 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐷 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝐷))
33	20, 32	syl5ibr 236	. . . . . . 7 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐵–1-1-onto→𝐷 → 𝑓 ∈ (𝐷 ↑𝑚 𝐵)))
34	33	abssdv 3676	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑𝑚 𝐵))
35		ovex 6678	. . . . . . 7 ⊢ (𝐷 ↑𝑚 𝐵) ∈ V
36	35	ssex 4802	. . . . . 6 ⊢ ({𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑𝑚 𝐵) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V)
37	34, 36	syl 17	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V)
38		f1oco 6159	. . . . . . . . 9 ⊢ ((ℎ:𝐶–1-1-onto→𝐷 ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
39	38	adantll 750	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
40		f1ocnv 6149	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → ◡𝑔:𝐵–1-1-onto→𝐴)
41	40	ad2antrr 762	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ◡𝑔:𝐵–1-1-onto→𝐴)
42		f1oco 6159	. . . . . . . 8 ⊢ (((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 ∧ ◡𝑔:𝐵–1-1-onto→𝐴) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
43	39, 41, 42	syl2anc 693	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
44	43	ex 450	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥:𝐴–1-1-onto→𝐶 → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷))
45		vex 3203	. . . . . . 7 ⊢ 𝑥 ∈ V
46		f1oeq1 6127	. . . . . . 7 ⊢ (𝑓 = 𝑥 → (𝑓:𝐴–1-1-onto→𝐶 ↔ 𝑥:𝐴–1-1-onto→𝐶))
47	45, 46	elab 3350	. . . . . 6 ⊢ (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ 𝑥:𝐴–1-1-onto→𝐶)
48	6, 45	coex 7118	. . . . . . . 8 ⊢ (ℎ ∘ 𝑥) ∈ V
49	10	cnvex 7113	. . . . . . . 8 ⊢ ◡𝑔 ∈ V
50	48, 49	coex 7118	. . . . . . 7 ⊢ ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ V
51		f1oeq1 6127	. . . . . . 7 ⊢ (𝑓 = ((ℎ ∘ 𝑥) ∘ ◡𝑔) → (𝑓:𝐵–1-1-onto→𝐷 ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷))
52	50, 51	elab 3350	. . . . . 6 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
53	44, 47, 52	3imtr4g 285	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} → ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}))
54		f1ocnv 6149	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ◡ℎ:𝐷–1-1-onto→𝐶)
55	54	ad2antlr 763	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → ◡ℎ:𝐷–1-1-onto→𝐶)
56		f1oco 6159	. . . . . . . . . 10 ⊢ ((𝑦:𝐵–1-1-onto→𝐷 ∧ 𝑔:𝐴–1-1-onto→𝐵) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
57	56	ancoms 469	. . . . . . . . 9 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
58	57	adantlr 751	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
59		f1oco 6159	. . . . . . . 8 ⊢ ((◡ℎ:𝐷–1-1-onto→𝐶 ∧ (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
60	55, 58, 59	syl2anc 693	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
61	60	ex 450	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦:𝐵–1-1-onto→𝐷 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶))
62		vex 3203	. . . . . . 7 ⊢ 𝑦 ∈ V
63		f1oeq1 6127	. . . . . . 7 ⊢ (𝑓 = 𝑦 → (𝑓:𝐵–1-1-onto→𝐷 ↔ 𝑦:𝐵–1-1-onto→𝐷))
64	62, 63	elab 3350	. . . . . 6 ⊢ (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ 𝑦:𝐵–1-1-onto→𝐷)
65	6	cnvex 7113	. . . . . . . 8 ⊢ ◡ℎ ∈ V
66	62, 10	coex 7118	. . . . . . . 8 ⊢ (𝑦 ∘ 𝑔) ∈ V
67	65, 66	coex 7118	. . . . . . 7 ⊢ (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ V
68		f1oeq1 6127	. . . . . . 7 ⊢ (𝑓 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) → (𝑓:𝐴–1-1-onto→𝐶 ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶))
69	67, 68	elab 3350	. . . . . 6 ⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
70	61, 64, 69	3imtr4g 285	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} → (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶}))
71	47, 64	anbi12i 733	. . . . . 6 ⊢ ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) ↔ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷))
72		coass 5654	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔))
73		f1ococnv1 6165	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴))
74	73	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴))
75	74	coeq2d 5284	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)))
76	39	adantrr 753	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
77		f1of 6137	. . . . . . . . . . . . 13 ⊢ ((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 → (ℎ ∘ 𝑥):𝐴⟶𝐷)
78		fcoi1 6078	. . . . . . . . . . . . 13 ⊢ ((ℎ ∘ 𝑥):𝐴⟶𝐷 → ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)) = (ℎ ∘ 𝑥))
79	76, 77, 78	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)) = (ℎ ∘ 𝑥))
80	75, 79	eqtrd 2656	. . . . . . . . . . 11 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = (ℎ ∘ 𝑥))
81	72, 80	syl5req 2669	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))
82		coass 5654	. . . . . . . . . . 11 ⊢ ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔)))
83		f1ococnv2 6163	. . . . . . . . . . . . . 14 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷))
84	83	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷))
85	84	coeq1d 5283	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)))
86	58	adantrl 752	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
87		f1of 6137	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷 → (𝑦 ∘ 𝑔):𝐴⟶𝐷)
88		fcoi2 6079	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∘ 𝑔):𝐴⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
89	86, 87, 88	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
90	85, 89	eqtrd 2656	. . . . . . . . . . 11 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
91	82, 90	syl5eqr 2670	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) = (𝑦 ∘ 𝑔))
92	81, 91	eqeq12d 2637	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔)))
93		eqcom 2629	. . . . . . . . 9 ⊢ ((((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))
94	92, 93	syl6bb 276	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔)))
95		f1of1 6136	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–1-1→𝐷)
96	95	ad2antlr 763	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ℎ:𝐶–1-1→𝐷)
97		f1of 6137	. . . . . . . . . 10 ⊢ (𝑥:𝐴–1-1-onto→𝐶 → 𝑥:𝐴⟶𝐶)
98	97	ad2antrl 764	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑥:𝐴⟶𝐶)
99	60	adantrl 752	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
100		f1of 6137	. . . . . . . . . 10 ⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶)
101	99, 100	syl 17	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶)
102		cocan1 6546	. . . . . . . . 9 ⊢ ((ℎ:𝐶–1-1→𝐷 ∧ 𝑥:𝐴⟶𝐶 ∧ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔))))
103	96, 98, 101, 102	syl3anc 1326	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔))))
104	26	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑔:𝐴–onto→𝐵)
105		f1ofn 6138	. . . . . . . . . 10 ⊢ (𝑦:𝐵–1-1-onto→𝐷 → 𝑦 Fn 𝐵)
106	105	ad2antll 765	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑦 Fn 𝐵)
107	43	adantrr 753	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
108		f1ofn 6138	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷 → ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵)
109	107, 108	syl 17	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵)
110		cocan2 6547	. . . . . . . . 9 ⊢ ((𝑔:𝐴–onto→𝐵 ∧ 𝑦 Fn 𝐵 ∧ ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
111	104, 106, 109, 110	syl3anc 1326	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
112	94, 103, 111	3bitr3d 298	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
113	112	ex 450	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))))
114	71, 113	syl5bi 232	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))))
115	19, 37, 53, 70, 114	en3d 7992	. . . 4 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
116	115	exlimivv 1860	. . 3 ⊢ (∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
117	3, 116	sylbir 225	. 2 ⊢ ((∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
118	1, 2, 117	syl2anb 496	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  Vcvv 3200   ⊆ wss 3574   class class class wbr 4653   I cid 5023  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   ↾ cres 5116   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –onto→wfo 5886  –1-1-onto→wf1o 5887  (class class class)co 6650   ↑_𝑚 cmap 7857   ≈ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859  df-en 7956

This theorem is referenced by:  poimirlem9  33418