Theorem mapfien 8196

Description: A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)

Hypotheses

Ref	Expression
mapfien.s	⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍}
mapfien.t	⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊}
mapfien.w	⊢ 𝑊 = (𝐺‘𝑍)
mapfien.f	⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
mapfien.g	⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)
mapfien.a	⊢ (𝜑 → 𝐴 ∈ V)
mapfien.b	⊢ (𝜑 → 𝐵 ∈ V)
mapfien.c	⊢ (𝜑 → 𝐶 ∈ V)
mapfien.d	⊢ (𝜑 → 𝐷 ∈ V)
mapfien.z	⊢ (𝜑 → 𝑍 ∈ 𝐵)

Assertion

Ref	Expression
mapfien	⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝑓,𝐹   𝑓,𝐺,𝑥   𝜑,𝑓   𝑥,𝐷   𝑆,𝑓   𝑇,𝑓   𝑥,𝑊   𝑥,𝑍

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑓)   𝐵(𝑓)   𝐶(𝑓)   𝐷(𝑓)   𝑆(𝑥)   𝑇(𝑥)   𝑊(𝑓)   𝑍(𝑓)

Proof of Theorem mapfien

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2610	. 2 ⊢ (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹)))
2		mapfien.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)
3		f1of 6050	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐷 → 𝐺:𝐵⟶𝐷)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐺:𝐵⟶𝐷)
5	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝐺:𝐵⟶𝐷)
6		breq1 4586	. . . . . . . . . 10 ⊢ (𝑥 = 𝑓 → (𝑥 finSupp 𝑍 ↔ 𝑓 finSupp 𝑍))
7		mapfien.s	. . . . . . . . . 10 ⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍}
8	6, 7	elrab2 3333	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑓 finSupp 𝑍))
9	8	simplbi 475	. . . . . . . 8 ⊢ (𝑓 ∈ 𝑆 → 𝑓 ∈ (𝐵 ↑𝑚 𝐴))
10	9	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓 ∈ (𝐵 ↑𝑚 𝐴))
11		elmapi 7765	. . . . . . 7 ⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) → 𝑓:𝐴⟶𝐵)
12	10, 11	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓:𝐴⟶𝐵)
13		mapfien.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
14		f1of 6050	. . . . . . . 8 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
15	13, 14	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
16	15	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝐹:𝐶⟶𝐴)
17		fco 5971	. . . . . 6 ⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝐹:𝐶⟶𝐴) → (𝑓 ∘ 𝐹):𝐶⟶𝐵)
18	12, 16, 17	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝑓 ∘ 𝐹):𝐶⟶𝐵)
19		fco 5971	. . . . 5 ⊢ ((𝐺:𝐵⟶𝐷 ∧ (𝑓 ∘ 𝐹):𝐶⟶𝐵) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)
20	5, 18, 19	syl2anc 691	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)
21		mapfien.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ V)
22		mapfien.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ V)
23	21, 22	elmapd 7758	. . . . 5 ⊢ (𝜑 → ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶) ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷))
24	23	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶) ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷))
25	20, 24	mpbird 246	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶))
26		mapfien.t	. . . 4 ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊}
27		mapfien.w	. . . 4 ⊢ 𝑊 = (𝐺‘𝑍)
28		mapfien.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
29		mapfien.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
30		mapfien.z	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
31	7, 26, 27, 13, 2, 28, 29, 22, 21, 30	mapfienlem1 8193	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊)
32		breq1 4586	. . . 4 ⊢ (𝑥 = (𝐺 ∘ (𝑓 ∘ 𝐹)) → (𝑥 finSupp 𝑊 ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊))
33	32, 26	elrab2 3333	. . 3 ⊢ ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ 𝑇 ↔ ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶) ∧ (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊))
34	25, 31, 33	sylanbrc 695	. 2 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ 𝑇)
35	7, 26, 27, 13, 2, 28, 29, 22, 21, 30	mapfienlem3 8195	. 2 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆)
36		coass 5571	. . . . . 6 ⊢ (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) = ((◡𝐺 ∘ 𝑔) ∘ (◡𝐹 ∘ 𝐹))
37	13	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐹:𝐶–1-1-onto→𝐴)
38		f1ococnv1 6078	. . . . . . . . 9 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐶))
39	37, 38	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐶))
40	39	coeq2d 5206	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ (◡𝐹 ∘ 𝐹)) = ((◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)))
41		f1ocnv 6062	. . . . . . . . . . . 12 ⊢ (𝐺:𝐵–1-1-onto→𝐷 → ◡𝐺:𝐷–1-1-onto→𝐵)
42		f1of 6050	. . . . . . . . . . . 12 ⊢ (◡𝐺:𝐷–1-1-onto→𝐵 → ◡𝐺:𝐷⟶𝐵)
43	2, 41, 42	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐺:𝐷⟶𝐵)
44	43	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ◡𝐺:𝐷⟶𝐵)
45		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ 𝑇)
46		breq1 4586	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑔 → (𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊))
47	46, 26	elrab2 3333	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ 𝑇 ↔ (𝑔 ∈ (𝐷 ↑𝑚 𝐶) ∧ 𝑔 finSupp 𝑊))
48	45, 47	sylib 207	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (𝑔 ∈ (𝐷 ↑𝑚 𝐶) ∧ 𝑔 finSupp 𝑊))
49	48	simpld 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ (𝐷 ↑𝑚 𝐶))
50		elmapi 7765	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐷 ↑𝑚 𝐶) → 𝑔:𝐶⟶𝐷)
51	49, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔:𝐶⟶𝐷)
52		fco 5971	. . . . . . . . . 10 ⊢ ((◡𝐺:𝐷⟶𝐵 ∧ 𝑔:𝐶⟶𝐷) → (◡𝐺 ∘ 𝑔):𝐶⟶𝐵)
53	44, 51, 52	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (◡𝐺 ∘ 𝑔):𝐶⟶𝐵)
54	53	adantrl 748	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐺 ∘ 𝑔):𝐶⟶𝐵)
55		fcoi1 5991	. . . . . . . 8 ⊢ ((◡𝐺 ∘ 𝑔):𝐶⟶𝐵 → ((◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)) = (◡𝐺 ∘ 𝑔))
56	54, 55	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)) = (◡𝐺 ∘ 𝑔))
57	40, 56	eqtrd 2644	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ (◡𝐹 ∘ 𝐹)) = (◡𝐺 ∘ 𝑔))
58	36, 57	syl5eq 2656	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) = (◡𝐺 ∘ 𝑔))
59	58	eqeq2d 2620	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ (𝑓 ∘ 𝐹) = (◡𝐺 ∘ 𝑔)))
60		coass 5571	. . . . . . 7 ⊢ ((◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹)))
61	2	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐺:𝐵–1-1-onto→𝐷)
62		f1ococnv1 6078	. . . . . . . . . 10 ⊢ (𝐺:𝐵–1-1-onto→𝐷 → (◡𝐺 ∘ 𝐺) = ( I ↾ 𝐵))
63	61, 62	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐺 ∘ 𝐺) = ( I ↾ 𝐵))
64	63	coeq1d 5205	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)))
65	18	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝑓 ∘ 𝐹):𝐶⟶𝐵)
66		fcoi2 5992	. . . . . . . . 9 ⊢ ((𝑓 ∘ 𝐹):𝐶⟶𝐵 → (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹))
67	65, 66	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹))
68	64, 67	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹))
69	60, 68	syl5eqr 2658	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∘ 𝐹))
70	69	eqeq2d 2620	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ (◡𝐺 ∘ 𝑔) = (𝑓 ∘ 𝐹)))
71		eqcom 2617	. . . . 5 ⊢ ((◡𝐺 ∘ 𝑔) = (𝑓 ∘ 𝐹) ↔ (𝑓 ∘ 𝐹) = (◡𝐺 ∘ 𝑔))
72	70, 71	syl6bb 275	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ (𝑓 ∘ 𝐹) = (◡𝐺 ∘ 𝑔)))
73	59, 72	bitr4d 270	. . 3 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ (◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹)))))
74		f1ofo 6057	. . . . 5 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
75	37, 74	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐹:𝐶–onto→𝐴)
76		ffn 5958	. . . . . 6 ⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴)
77	10, 11, 76	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓 Fn 𝐴)
78	77	adantrr 749	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝑓 Fn 𝐴)
79		f1ocnv 6062	. . . . . . . . 9 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐶)
80		f1of 6050	. . . . . . . . 9 ⊢ (◡𝐹:𝐴–1-1-onto→𝐶 → ◡𝐹:𝐴⟶𝐶)
81	13, 79, 80	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ◡𝐹:𝐴⟶𝐶)
82	81	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ◡𝐹:𝐴⟶𝐶)
83		fco 5971	. . . . . . 7 ⊢ (((◡𝐺 ∘ 𝑔):𝐶⟶𝐵 ∧ ◡𝐹:𝐴⟶𝐶) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹):𝐴⟶𝐵)
84	53, 82, 83	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹):𝐴⟶𝐵)
85		ffn 5958	. . . . . 6 ⊢ (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹):𝐴⟶𝐵 → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴)
86	84, 85	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴)
87	86	adantrl 748	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴)
88		cocan2 6447	. . . 4 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑓 Fn 𝐴 ∧ ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ 𝑓 = ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹)))
89	75, 78, 87, 88	syl3anc 1318	. . 3 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ 𝑓 = ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹)))
90	2, 41	syl 17	. . . . . 6 ⊢ (𝜑 → ◡𝐺:𝐷–1-1-onto→𝐵)
91	90	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ◡𝐺:𝐷–1-1-onto→𝐵)
92		f1of1 6049	. . . . 5 ⊢ (◡𝐺:𝐷–1-1-onto→𝐵 → ◡𝐺:𝐷–1-1→𝐵)
93	91, 92	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ◡𝐺:𝐷–1-1→𝐵)
94	51	adantrl 748	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝑔:𝐶⟶𝐷)
95	20	adantrr 749	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)
96		cocan1 6446	. . . 4 ⊢ ((◡𝐺:𝐷–1-1→𝐵 ∧ 𝑔:𝐶⟶𝐷 ∧ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹))))
97	93, 94, 95, 96	syl3anc 1318	. . 3 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹))))
98	73, 89, 97	3bitr3d 297	. 2 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝑓 = ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹))))
99	1, 34, 35, 98	f1o2d 6785	1 ⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173   class class class wbr 4583   ↦ cmpt 4643   I cid 4948  ^◡ccnv 5037   ↾ cres 5040   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↑_𝑚 cmap 7744   finSupp cfsupp 8158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-1o 7447  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-fin 7845  df-fsupp 8159

This theorem is referenced by:  mapfien2  8197  wemapwe  8477  oef1o  8478  fcobijfs  28889