Theorem fpwrelmap 33395

Description: Define a canonical mapping between functions from 𝐴 into subsets of 𝐵 and the relations with domain 𝐴 and range within 𝐵. Note that the same relation is used in axdc2lem 10553 and marypha2lem1 9454. (Contributed by Thierry Arnoux, 28-Aug-2017.)

Hypotheses

Ref	Expression
fpwrelmap.1	⊢ 𝐴 ∈ V
fpwrelmap.2	⊢ 𝐵 ∈ V
fpwrelmap.3	⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})

Assertion

Ref	Expression
fpwrelmap	⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)⟶1-1onto𝒫 (𝐴 × 𝐵)

Distinct variable groups:   𝑥,𝑓,𝑦,𝐴   𝐵,𝑓,𝑥,𝑦

Allowed substitution hints:   𝑀(𝑥, 𝑦, 𝑓)

Proof of Theorem fpwrelmap

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwrelmap.3	. . 3 ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
2		fpwrelmap.1	. . . . . 6 ⊢ 𝐴 ∈ V
3	2	a1i 11	. . . . 5 ⊢ (⊤ → 𝐴 ∈ V)
4		abid2 2901	. . . . . . 7 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥)
5	4	fvexi 6922	. . . . . 6 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V
6	5	a1i 11	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
7	3, 6	opabex3d 8001	. . . 4 ⊢ (⊤ → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
8	7	adantr 486	. . 3 ⊢ ((⊤ ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
9	2	mptex 7252	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V
10	9	a1i 11	. . 3 ⊢ ((⊤ ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V)
11		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ (𝑓‘𝑥))
12		elmapi 8897	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
13	12	ffvelcdmda 7108	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
14	13	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
15		elelpwi 4570	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ∈ 𝒫 𝐵) → 𝑦 ∈ 𝐵)
16	11, 14, 15	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
17	16	ex 418	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
18	17	imdistanda 582	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
19	18	ssopab2dv 5530	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
20	19	adantr 486	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21		simpr 490	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
22		df-xp 5661	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
24	20, 21, 23	3sstr4d 3968	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ⊆ (𝐴 × 𝐵))
25		velpw 4565	. . . . . . 7 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↔ 𝑟 ⊆ (𝐴 × 𝐵))
26	24, 25	sylibr 237	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
27	12	feqmptd 6976	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
28	27	adantr 486	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
29		nfv 1949	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)
30		nfopab1 5178	. . . . . . . . . 10 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
31	30	nfeq2 2943	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
32	29, 31	nfan 1934	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
33		df-rab 3417	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}
34	33	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
35		nfv 1949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)
36		nfopab2 5179	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
37	36	nfeq2 2943	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
38	35, 37	nfan 1934	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
39		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
40	38, 39	nfan 1934	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴)
41	16	adantllr 732	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
42		df-br 5107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
43		eleq2 2853	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
44		opabidw 5502	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
45	43, 44	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
46	42, 45	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
47	46	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
48		elfvdm 6942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ dom 𝑓)
49	48	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ dom 𝑓)
50	12	fdmd 6742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → dom 𝑓 = 𝐴)
51	50	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → dom 𝑓 = 𝐴)
52	49, 51	eleqtrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ 𝐴)
53	52	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ 𝐴))
54	53	pm4.71rd 572	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
55	54	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
56	47, 55	bitr4d 285	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ 𝑦 ∈ (𝑓‘𝑥)))
57	56	biimpar 483	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
58	41, 57	jca 521	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
59	58	ex 418	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
60	56	biimpd 232	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 → 𝑦 ∈ (𝑓‘𝑥)))
61	60	adantld 496	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥)))
62	59, 61	impbid 215	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
63	40, 62	abbid 2831	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
64	4	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥))
65	34, 63, 64	3eqtr2rd 2805	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
66	32, 65	mpteq2da 5200	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
67	28, 66	eqtrd 2798	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
68	26, 67	jca 521	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
69		fpwrelmap.2	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
70		ssrab2 4008	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
71	69, 70	elpwi2 5301	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵
72	71	a1i 11	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
73	72	fmpttd 7139	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
74	73	adantr 486	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
75		simpr 490	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
76	75	feq1d 6713	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓:𝐴⟶𝒫 𝐵 ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
77	74, 76	mpbird 260	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓:𝐴⟶𝒫 𝐵)
78	69	pwex 5346	. . . . . . . 8 ⊢ 𝒫 𝐵 ∈ V
79	78, 2	elmap 8927	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)
80	77, 79	sylibr 237	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))
81		elpwi 4567	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → 𝑟 ⊆ (𝐴 × 𝐵))
82	81	adantr 486	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
83		xpss 5671	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
84	82, 83	sstrdi 3925	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
85		df-rel 5662	. . . . . . . 8 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
86	84, 85	sylibr 237	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
87		relopab 5808	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
88	87	a1i 11	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
89		id 23	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
90		nfv 1949	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
91		nfmpt1 5207	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
92	91	nfeq2 2943	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
93	90, 92	nfan 1934	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
94		nfv 1949	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
95	39	nfci 2914	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
96		nfrab1 3435	. . . . . . . . . . 11 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}
97	95, 96	nfmpt 5206	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
98	97	nfeq2 2943	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
99	94, 98	nfan 1934	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
100		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑥𝑟
101		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑦𝑟
102		brelg 33273	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
103	81, 102	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
104	103	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
105	104	simpld 500	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥 ∈ 𝐴)
106	104	simprd 501	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ 𝐵)
107		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥𝑟𝑦)
108	75	fveq1d 6910	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓‘𝑥) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥))
109	69	rabex 5304	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V
110		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
111	110	fvmpt2 7028	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
112	109, 111	mpan2 704	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
113	108, 112	sylan9eq 2818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
114	113	eleq2d 2850	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
115		rabid 3436	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
116	114, 115	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
117	105, 116	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
118	106, 107, 117	mpbir2and 726	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥))
119	105, 118	jca 521	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
120	119	ex 418	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
121	116	simplbda 505	. . . . . . . . . . . 12 ⊢ ((((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
122	121	expl 463	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦))
123	120, 122	impbid 215	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
124	42, 123	bitr3id 288	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
125	124, 44	bitr4di 292	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
126	93, 99, 100, 101, 30, 36, 125	eqrelrd2 33282	. . . . . . 7 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
127	86, 88, 89, 126	syl21anc 851	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
128	80, 127	jca 521	. . . . 5 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
129	68, 128	impbii 212	. . . 4 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
130	129	a1i 11	. . 3 ⊢ (⊤ → ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))))
131	1, 8, 10, 130	f1od 7697	. 2 ⊢ (⊤ → 𝑀:(𝒫 𝐵 ↑m 𝐴)⟶1-1onto𝒫 (𝐴 × 𝐵))
132	131	mptru 1577	1 ⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)⟶1-1onto𝒫 (𝐴 × 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2147  {cab 2741  {crab 3416  Vcvv 3454   ⊆ wss 3900  𝒫 cpw 4560  ⟨cop 4838   class class class wbr 5106  {copab 5170   ↦ cmpt 5189   × cxp 5653  dom cdm 5655  Rel wrel 5660  ⟶wf 6554  ⟶1-1ontowf1o 6557  ‘cfv 6558  (class class class)co 7443   ↑_m cmap 8875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1st 8025  df-2nd 8026  df-map 8877

This theorem is used by:  fpwrelmapffs  33396