Theorem hashfacenOLD 14352

Description: Obsolete version of hashfacen 14351 as of 7-Aug-2024. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

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

Proof of Theorem hashfacenOLD

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

Step	Hyp	Ref	Expression
1		bren 8893	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑔 𝑔:𝐴–1-1-onto→𝐵)
2		bren 8893	. 2 ⊢ (𝐶 ≈ 𝐷 ↔ ∃ℎ ℎ:𝐶–1-1-onto→𝐷)
3		exdistrv 1959	. . 3 ⊢ (∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ↔ (∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷))
4		f1of 6784	. . . . . . . 8 ⊢ (𝑓:𝐴–1-1-onto→𝐶 → 𝑓:𝐴⟶𝐶)
5		f1odm 6788	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → dom ℎ = 𝐶)
6		vex 3449	. . . . . . . . . . 11 ⊢ ℎ ∈ V
7	6	dmex 7848	. . . . . . . . . 10 ⊢ dom ℎ ∈ V
8	5, 7	eqeltrrdi 2847	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐶 ∈ V)
9		f1odm 6788	. . . . . . . . . 10 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → dom 𝑔 = 𝐴)
10		vex 3449	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
11	10	dmex 7848	. . . . . . . . . 10 ⊢ dom 𝑔 ∈ V
12	9, 11	eqeltrrdi 2847	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
13		elmapg 8778	. . . . . . . . 9 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝑓 ∈ (𝐶 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝐶))
14	8, 12, 13	syl2anr 597	. . . . . . . 8 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐶 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝐶))
15	4, 14	syl5ibr 245	. . . . . . 7 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐴–1-1-onto→𝐶 → 𝑓 ∈ (𝐶 ↑m 𝐴)))
16	15	abssdv 4025	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑m 𝐴))
17		ovex 7390	. . . . . . 7 ⊢ (𝐶 ↑m 𝐴) ∈ V
18	17	ssex 5278	. . . . . 6 ⊢ ({𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑m 𝐴) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V)
19	16, 18	syl 17	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V)
20		f1of 6784	. . . . . . . 8 ⊢ (𝑓:𝐵–1-1-onto→𝐷 → 𝑓:𝐵⟶𝐷)
21		f1ofo 6791	. . . . . . . . . . 11 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–onto→𝐷)
22		forn 6759	. . . . . . . . . . 11 ⊢ (ℎ:𝐶–onto→𝐷 → ran ℎ = 𝐷)
23	21, 22	syl 17	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ran ℎ = 𝐷)
24	6	rnex 7849	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
25	23, 24	eqeltrrdi 2847	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐷 ∈ V)
26		f1ofo 6791	. . . . . . . . . . 11 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝑔:𝐴–onto→𝐵)
27		forn 6759	. . . . . . . . . . 11 ⊢ (𝑔:𝐴–onto→𝐵 → ran 𝑔 = 𝐵)
28	26, 27	syl 17	. . . . . . . . . 10 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → ran 𝑔 = 𝐵)
29	10	rnex 7849	. . . . . . . . . 10 ⊢ ran 𝑔 ∈ V
30	28, 29	eqeltrrdi 2847	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
31		elmapg 8778	. . . . . . . . 9 ⊢ ((𝐷 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ (𝐷 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐷))
32	25, 30, 31	syl2anr 597	. . . . . . . 8 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐷 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐷))
33	20, 32	syl5ibr 245	. . . . . . 7 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐵–1-1-onto→𝐷 → 𝑓 ∈ (𝐷 ↑m 𝐵)))
34	33	abssdv 4025	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑m 𝐵))
35		ovex 7390	. . . . . . 7 ⊢ (𝐷 ↑m 𝐵) ∈ V
36	35	ssex 5278	. . . . . 6 ⊢ ({𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑m 𝐵) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V)
37	34, 36	syl 17	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V)
38		f1oco 6807	. . . . . . . . 9 ⊢ ((ℎ:𝐶–1-1-onto→𝐷 ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
39	38	adantll 712	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
40		f1ocnv 6796	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → ◡𝑔:𝐵–1-1-onto→𝐴)
41	40	ad2antrr 724	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ◡𝑔:𝐵–1-1-onto→𝐴)
42		f1oco 6807	. . . . . . . 8 ⊢ (((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 ∧ ◡𝑔:𝐵–1-1-onto→𝐴) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
43	39, 41, 42	syl2anc 584	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
44	43	ex 413	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥:𝐴–1-1-onto→𝐶 → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷))
45		vex 3449	. . . . . . 7 ⊢ 𝑥 ∈ V
46		f1oeq1 6772	. . . . . . 7 ⊢ (𝑓 = 𝑥 → (𝑓:𝐴–1-1-onto→𝐶 ↔ 𝑥:𝐴–1-1-onto→𝐶))
47	45, 46	elab 3630	. . . . . 6 ⊢ (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ 𝑥:𝐴–1-1-onto→𝐶)
48	6, 45	coex 7867	. . . . . . . 8 ⊢ (ℎ ∘ 𝑥) ∈ V
49	10	cnvex 7862	. . . . . . . 8 ⊢ ◡𝑔 ∈ V
50	48, 49	coex 7867	. . . . . . 7 ⊢ ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ V
51		f1oeq1 6772	. . . . . . 7 ⊢ (𝑓 = ((ℎ ∘ 𝑥) ∘ ◡𝑔) → (𝑓:𝐵–1-1-onto→𝐷 ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷))
52	50, 51	elab 3630	. . . . . 6 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
53	44, 47, 52	3imtr4g 295	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} → ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}))
54		f1ocnv 6796	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ◡ℎ:𝐷–1-1-onto→𝐶)
55	54	ad2antlr 725	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → ◡ℎ:𝐷–1-1-onto→𝐶)
56		f1oco 6807	. . . . . . . . . 10 ⊢ ((𝑦:𝐵–1-1-onto→𝐷 ∧ 𝑔:𝐴–1-1-onto→𝐵) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
57	56	ancoms 459	. . . . . . . . 9 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
58	57	adantlr 713	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
59		f1oco 6807	. . . . . . . 8 ⊢ ((◡ℎ:𝐷–1-1-onto→𝐶 ∧ (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
60	55, 58, 59	syl2anc 584	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
61	60	ex 413	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦:𝐵–1-1-onto→𝐷 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶))
62		vex 3449	. . . . . . 7 ⊢ 𝑦 ∈ V
63		f1oeq1 6772	. . . . . . 7 ⊢ (𝑓 = 𝑦 → (𝑓:𝐵–1-1-onto→𝐷 ↔ 𝑦:𝐵–1-1-onto→𝐷))
64	62, 63	elab 3630	. . . . . 6 ⊢ (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ 𝑦:𝐵–1-1-onto→𝐷)
65	6	cnvex 7862	. . . . . . . 8 ⊢ ◡ℎ ∈ V
66	62, 10	coex 7867	. . . . . . . 8 ⊢ (𝑦 ∘ 𝑔) ∈ V
67	65, 66	coex 7867	. . . . . . 7 ⊢ (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ V
68		f1oeq1 6772	. . . . . . 7 ⊢ (𝑓 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) → (𝑓:𝐴–1-1-onto→𝐶 ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶))
69	67, 68	elab 3630	. . . . . 6 ⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
70	61, 64, 69	3imtr4g 295	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} → (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶}))
71	47, 64	anbi12i 627	. . . . . 6 ⊢ ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) ↔ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷))
72		coass 6217	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔))
73		f1ococnv1 6813	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴))
74	73	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴))
75	74	coeq2d 5818	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)))
76	39	adantrr 715	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
77		f1of 6784	. . . . . . . . . . . . 13 ⊢ ((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 → (ℎ ∘ 𝑥):𝐴⟶𝐷)
78		fcoi1 6716	. . . . . . . . . . . . 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 2776	. . . . . . . . . . 11 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = (ℎ ∘ 𝑥))
81	72, 80	eqtr2id 2789	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))
82		coass 6217	. . . . . . . . . . 11 ⊢ ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔)))
83		f1ococnv2 6811	. . . . . . . . . . . . . 14 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷))
84	83	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷))
85	84	coeq1d 5817	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)))
86	58	adantrl 714	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
87		f1of 6784	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷 → (𝑦 ∘ 𝑔):𝐴⟶𝐷)
88		fcoi2 6717	. . . . . . . . . . . . 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 2776	. . . . . . . . . . 11 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
91	82, 90	eqtr3id 2790	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) = (𝑦 ∘ 𝑔))
92	81, 91	eqeq12d 2752	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔)))
93		eqcom 2743	. . . . . . . . 9 ⊢ ((((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))
94	92, 93	bitrdi 286	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔)))
95		f1of1 6783	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–1-1→𝐷)
96	95	ad2antlr 725	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ℎ:𝐶–1-1→𝐷)
97		f1of 6784	. . . . . . . . . 10 ⊢ (𝑥:𝐴–1-1-onto→𝐶 → 𝑥:𝐴⟶𝐶)
98	97	ad2antrl 726	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑥:𝐴⟶𝐶)
99	60	adantrl 714	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
100		f1of 6784	. . . . . . . . . 10 ⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶)
101	99, 100	syl 17	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶)
102		cocan1 7237	. . . . . . . . 9 ⊢ ((ℎ:𝐶–1-1→𝐷 ∧ 𝑥:𝐴⟶𝐶 ∧ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔))))
103	96, 98, 101, 102	syl3anc 1371	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔))))
104	26	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑔:𝐴–onto→𝐵)
105		f1ofn 6785	. . . . . . . . . 10 ⊢ (𝑦:𝐵–1-1-onto→𝐷 → 𝑦 Fn 𝐵)
106	105	ad2antll 727	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑦 Fn 𝐵)
107	43	adantrr 715	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
108		f1ofn 6785	. . . . . . . . . 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 7238	. . . . . . . . 9 ⊢ ((𝑔:𝐴–onto→𝐵 ∧ 𝑦 Fn 𝐵 ∧ ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
111	104, 106, 109, 110	syl3anc 1371	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
112	94, 103, 111	3bitr3d 308	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
113	112	ex 413	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))))
114	71, 113	biimtrid 241	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))))
115	19, 37, 53, 70, 114	en3d 8929	. . . 4 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
116	115	exlimivv 1935	. . 3 ⊢ (∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
117	3, 116	sylbir 234	. 2 ⊢ ((∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
118	1, 2, 117	syl2anb 598	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713  Vcvv 3445   ⊆ wss 3910   class class class wbr 5105   I cid 5530  ^◡ccnv 5632  dom cdm 5633  ran crn 5634   ↾ cres 5635   ∘ ccom 5637   Fn wfn 6491  ⟶wf 6492  –1-1→wf1 6493  –onto→wfo 6494  –1-1-onto→wf1o 6495  (class class class)co 7357   ↑_m cmap 8765   ≈ cen 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-map 8767  df-en 8884

This theorem is referenced by: (None)