mapfien - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mapfien		Structured version Visualization version GIF version

Theorem mapfien 9344

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.) (Revised by AV, 28-Jul-2024.)

**Hypotheses**
Ref	Expression
mapfien.s	⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑_m 𝐴) ∣ 𝑥 finSupp 𝑍}
mapfien.t	⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑_m 𝐶) ∣ 𝑥 finSupp 𝑊}
mapfien.w	⊢ 𝑊 = (𝐺‘𝑍)
mapfien.f	⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
mapfien.g	⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)
mapfien.a	⊢ (𝜑 → 𝐴 ∈ 𝑈)
mapfien.b	⊢ (𝜑 → 𝐵 ∈ 𝑉)
mapfien.c	⊢ (𝜑 → 𝐶 ∈ 𝑋)
mapfien.d	⊢ (𝜑 → 𝐷 ∈ 𝑌)
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 2736	. 2 ⊢ (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹)))
2		mapfien.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)
3		f1of 6784	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐷 → 𝐺:𝐵⟶𝐷)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐺:𝐵⟶𝐷)
5	4	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝐺:𝐵⟶𝐷)
6		breq1 5108	. . . . . . . . . 10 ⊢ (𝑥 = 𝑓 → (𝑥 finSupp 𝑍 ↔ 𝑓 finSupp 𝑍))
7		mapfien.s	. . . . . . . . . 10 ⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑_m 𝐴) ∣ 𝑥 finSupp 𝑍}
8	6, 7	elrab2 3648	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ (𝐵 ↑_m 𝐴) ∧ 𝑓 finSupp 𝑍))
9	8	simplbi 498	. . . . . . . 8 ⊢ (𝑓 ∈ 𝑆 → 𝑓 ∈ (𝐵 ↑_m 𝐴))
10	9	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓 ∈ (𝐵 ↑_m 𝐴))
11		elmapi 8787	. . . . . . 7 ⊢ (𝑓 ∈ (𝐵 ↑_m 𝐴) → 𝑓:𝐴⟶𝐵)
12	10, 11	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓:𝐴⟶𝐵)
13		mapfien.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
14		f1of 6784	. . . . . . . 8 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
15	13, 14	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
16	15	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝐹:𝐶⟶𝐴)
17	12, 16	fcod 6694	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝑓 ∘ 𝐹):𝐶⟶𝐵)
18	5, 17	fcod 6694	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)
19		mapfien.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑌)
20		mapfien.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
21	19, 20	elmapd 8779	. . . . 5 ⊢ (𝜑 → ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑_m 𝐶) ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷))
22	21	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑_m 𝐶) ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷))
23	18, 22	mpbird 256	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑_m 𝐶))
24		mapfien.t	. . . 4 ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑_m 𝐶) ∣ 𝑥 finSupp 𝑊}
25		mapfien.w	. . . 4 ⊢ 𝑊 = (𝐺‘𝑍)
26		mapfien.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
27		mapfien.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
28		mapfien.z	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
29	7, 24, 25, 13, 2, 26, 27, 20, 19, 28	mapfienlem1 9341	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊)
30		breq1 5108	. . . 4 ⊢ (𝑥 = (𝐺 ∘ (𝑓 ∘ 𝐹)) → (𝑥 finSupp 𝑊 ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊))
31	30, 24	elrab2 3648	. . 3 ⊢ ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ 𝑇 ↔ ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑_m 𝐶) ∧ (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊))
32	23, 29, 31	sylanbrc 583	. 2 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ 𝑇)
33	7, 24, 25, 13, 2, 26, 27, 20, 19, 28	mapfienlem3 9343	. 2 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∈ 𝑆)
34		coass 6217	. . . . . 6 ⊢ (((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∘ 𝐹) = ((^◡𝐺 ∘ 𝑔) ∘ (^◡𝐹 ∘ 𝐹))
35	13	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐹:𝐶–1-1-onto→𝐴)
36		f1ococnv1 6813	. . . . . . . . 9 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐶))
37	35, 36	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐶))
38	37	coeq2d 5818	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) ∘ (^◡𝐹 ∘ 𝐹)) = ((^◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)))
39		f1ocnv 6796	. . . . . . . . . . . 12 ⊢ (𝐺:𝐵–1-1-onto→𝐷 → ^◡𝐺:𝐷–1-1-onto→𝐵)
40		f1of 6784	. . . . . . . . . . . 12 ⊢ (^◡𝐺:𝐷–1-1-onto→𝐵 → ^◡𝐺:𝐷⟶𝐵)
41	2, 39, 40	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐺:𝐷⟶𝐵)
42	41	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ^◡𝐺:𝐷⟶𝐵)
43		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ 𝑇)
44		breq1 5108	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑔 → (𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊))
45	44, 24	elrab2 3648	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ 𝑇 ↔ (𝑔 ∈ (𝐷 ↑_m 𝐶) ∧ 𝑔 finSupp 𝑊))
46	43, 45	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (𝑔 ∈ (𝐷 ↑_m 𝐶) ∧ 𝑔 finSupp 𝑊))
47	46	simpld 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ (𝐷 ↑_m 𝐶))
48		elmapi 8787	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐷 ↑_m 𝐶) → 𝑔:𝐶⟶𝐷)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔:𝐶⟶𝐷)
50	42, 49	fcod 6694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (^◡𝐺 ∘ 𝑔):𝐶⟶𝐵)
51	50	adantrl 714	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (^◡𝐺 ∘ 𝑔):𝐶⟶𝐵)
52		fcoi1 6716	. . . . . . . 8 ⊢ ((^◡𝐺 ∘ 𝑔):𝐶⟶𝐵 → ((^◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)) = (^◡𝐺 ∘ 𝑔))
53	51, 52	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)) = (^◡𝐺 ∘ 𝑔))
54	38, 53	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) ∘ (^◡𝐹 ∘ 𝐹)) = (^◡𝐺 ∘ 𝑔))
55	34, 54	eqtrid 2788	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∘ 𝐹) = (^◡𝐺 ∘ 𝑔))
56	55	eqeq2d 2747	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∘ 𝐹) ↔ (𝑓 ∘ 𝐹) = (^◡𝐺 ∘ 𝑔)))
57		coass 6217	. . . . . . 7 ⊢ ((^◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹)))
58	2	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐺:𝐵–1-1-onto→𝐷)
59		f1ococnv1 6813	. . . . . . . . . 10 ⊢ (𝐺:𝐵–1-1-onto→𝐷 → (^◡𝐺 ∘ 𝐺) = ( I ↾ 𝐵))
60	58, 59	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (^◡𝐺 ∘ 𝐺) = ( I ↾ 𝐵))
61	60	coeq1d 5817	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)))
62	17	adantrr 715	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝑓 ∘ 𝐹):𝐶⟶𝐵)
63		fcoi2 6717	. . . . . . . . 9 ⊢ ((𝑓 ∘ 𝐹):𝐶⟶𝐵 → (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹))
64	62, 63	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹))
65	61, 64	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹))
66	57, 65	eqtr3id 2790	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∘ 𝐹))
67	66	eqeq2d 2747	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) = (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ (^◡𝐺 ∘ 𝑔) = (𝑓 ∘ 𝐹)))
68		eqcom 2743	. . . . 5 ⊢ ((^◡𝐺 ∘ 𝑔) = (𝑓 ∘ 𝐹) ↔ (𝑓 ∘ 𝐹) = (^◡𝐺 ∘ 𝑔))
69	67, 68	bitrdi 286	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) = (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ (𝑓 ∘ 𝐹) = (^◡𝐺 ∘ 𝑔)))
70	56, 69	bitr4d 281	. . 3 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∘ 𝐹) ↔ (^◡𝐺 ∘ 𝑔) = (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹)))))
71		f1ofo 6791	. . . . 5 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
72	35, 71	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐹:𝐶–onto→𝐴)
73		ffn 6668	. . . . . 6 ⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴)
74	10, 11, 73	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓 Fn 𝐴)
75	74	adantrr 715	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝑓 Fn 𝐴)
76		f1ocnv 6796	. . . . . . . . 9 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ^◡𝐹:𝐴–1-1-onto→𝐶)
77		f1of 6784	. . . . . . . . 9 ⊢ (^◡𝐹:𝐴–1-1-onto→𝐶 → ^◡𝐹:𝐴⟶𝐶)
78	13, 76, 77	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:𝐴⟶𝐶)
79	78	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ^◡𝐹:𝐴⟶𝐶)
80	50, 79	fcod 6694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹):𝐴⟶𝐵)
81	80	ffnd 6669	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) Fn 𝐴)
82	81	adantrl 714	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) Fn 𝐴)
83		cocan2 7238	. . . 4 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑓 Fn 𝐴 ∧ ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) Fn 𝐴) → ((𝑓 ∘ 𝐹) = (((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∘ 𝐹) ↔ 𝑓 = ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹)))
84	72, 75, 82, 83	syl3anc 1371	. . 3 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ∘ 𝐹) ↔ 𝑓 = ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹)))
85	2, 39	syl 17	. . . . . 6 ⊢ (𝜑 → ^◡𝐺:𝐷–1-1-onto→𝐵)
86	85	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ^◡𝐺:𝐷–1-1-onto→𝐵)
87		f1of1 6783	. . . . 5 ⊢ (^◡𝐺:𝐷–1-1-onto→𝐵 → ^◡𝐺:𝐷–1-1→𝐵)
88	86, 87	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ^◡𝐺:𝐷–1-1→𝐵)
89	49	adantrl 714	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝑔:𝐶⟶𝐷)
90	18	adantrr 715	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)
91		cocan1 7237	. . . 4 ⊢ ((^◡𝐺:𝐷–1-1→𝐵 ∧ 𝑔:𝐶⟶𝐷 ∧ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷) → ((^◡𝐺 ∘ 𝑔) = (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹))))
92	88, 89, 90, 91	syl3anc 1371	. . 3 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((^◡𝐺 ∘ 𝑔) = (^◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹))))
93	70, 84, 92	3bitr3d 308	. 2 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝑓 = ((^◡𝐺 ∘ 𝑔) ∘ ^◡𝐹) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹))))
94	1, 32, 33, 93	f1o2d 7607	1 ⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {crab 3407 class class class wbr 5105 ↦ cmpt 5188 I cid 5530 ^◡ccnv 5632 ↾ cres 5635 ∘ ccom 5637 Fn wfn 6491 ⟶wf 6492 –1-1→wf1 6493 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 ↑_m cmap 8765 finSupp cfsupp 9305

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-rep 5242 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-3or 1088 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-reu 3354 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-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 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-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 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-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-1o 8412 df-map 8767 df-en 8884 df-fin 8887 df-fsupp 9306

This theorem is referenced by: mapfien2 9345 wemapwe 9633 oef1o 9634 fcobijfs 31640

W3C validator