Theorem fpwrelmap 32793

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 10362 and marypha2lem1 9342. (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-1-onto→𝒫 (𝐴 × 𝐵)

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 2874	. . . . . . 7 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥)
5	4	fvexi 6849	. . . . . 6 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V
6	5	a1i 11	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
7	3, 6	opabex3d 7911	. . . 4 ⊢ (⊤ → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
8	7	adantr 480	. . 3 ⊢ ((⊤ ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
9	2	mptex 7171	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V
10	9	a1i 11	. . 3 ⊢ ((⊤ ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V)
11		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ (𝑓‘𝑥))
12		elmapi 8790	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
13	12	ffvelcdmda 7031	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
14	13	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
15		elelpwi 4565	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ∈ 𝒫 𝐵) → 𝑦 ∈ 𝐵)
16	11, 14, 15	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
17	16	ex 412	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
18	17	imdistanda 571	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
19	18	ssopab2dv 5500	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
20	19	adantr 480	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
21		simpr 484	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
22		df-xp 5631	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
24	20, 21, 23	3sstr4d 3990	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ⊆ (𝐴 × 𝐵))
25		velpw 4560	. . . . . . 7 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↔ 𝑟 ⊆ (𝐴 × 𝐵))
26	24, 25	sylibr 234	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
27	12	feqmptd 6903	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
28	27	adantr 480	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
29		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)
30		nfopab1 5169	. . . . . . . . . 10 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
31	30	nfeq2 2917	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
32	29, 31	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
33		df-rab 3401	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}
34	33	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
35		nfv 1916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)
36		nfopab2 5170	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
37	36	nfeq2 2917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
38	35, 37	nfan 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
39		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
40	38, 39	nfan 1901	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴)
41	16	adantllr 720	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
42		df-br 5100	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
43		eleq2 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
44		opabidw 5473	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
45	43, 44	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
46	42, 45	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
47	46	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
48		elfvdm 6869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ dom 𝑓)
49	48	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ dom 𝑓)
50	12	fdmd 6673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → dom 𝑓 = 𝐴)
51	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → dom 𝑓 = 𝐴)
52	49, 51	eleqtrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ 𝐴)
53	52	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ 𝐴))
54	53	pm4.71rd 562	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
55	54	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
56	47, 55	bitr4d 282	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ 𝑦 ∈ (𝑓‘𝑥)))
57	56	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
58	41, 57	jca 511	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
59	58	ex 412	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
60	56	biimpd 229	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 → 𝑦 ∈ (𝑓‘𝑥)))
61	60	adantld 490	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥)))
62	59, 61	impbid 212	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
63	40, 62	abbid 2805	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
64	4	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥))
65	34, 63, 64	3eqtr2rd 2779	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
66	32, 65	mpteq2da 5191	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
67	28, 66	eqtrd 2772	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
68	26, 67	jca 511	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
69		fpwrelmap.2	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
70		ssrab2 4033	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
71	69, 70	elpwi2 5281	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵
72	71	a1i 11	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
73	72	fmpttd 7062	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
74	73	adantr 480	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
75		simpr 484	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
76	75	feq1d 6645	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓:𝐴⟶𝒫 𝐵 ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
77	74, 76	mpbird 257	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓:𝐴⟶𝒫 𝐵)
78	69	pwex 5326	. . . . . . . 8 ⊢ 𝒫 𝐵 ∈ V
79	78, 2	elmap 8813	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)
80	77, 79	sylibr 234	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))
81		elpwi 4562	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → 𝑟 ⊆ (𝐴 × 𝐵))
82	81	adantr 480	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
83		xpss 5641	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
84	82, 83	sstrdi 3947	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
85		df-rel 5632	. . . . . . . 8 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
86	84, 85	sylibr 234	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
87		relopabv 5771	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
88	87	a1i 11	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
89		id 22	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
90		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
91		nfmpt1 5198	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
92	91	nfeq2 2917	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
93	90, 92	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
94		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
95	39	nfci 2887	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
96		nfrab1 3420	. . . . . . . . . . 11 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}
97	95, 96	nfmpt 5197	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
98	97	nfeq2 2917	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
99	94, 98	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
100		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥𝑟
101		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑦𝑟
102		brelg 32667	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
103	81, 102	sylan 581	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
104	103	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
105	104	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥 ∈ 𝐴)
106	104	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ 𝐵)
107		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥𝑟𝑦)
108	75	fveq1d 6837	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓‘𝑥) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥))
109	69	rabex 5285	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V
110		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
111	110	fvmpt2 6954	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
112	109, 111	mpan2 692	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
113	108, 112	sylan9eq 2792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
114	113	eleq2d 2823	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
115		rabid 3421	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
116	114, 115	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
117	105, 116	syldan 592	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
118	106, 107, 117	mpbir2and 714	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥))
119	105, 118	jca 511	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
120	119	ex 412	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
121	116	simplbda 499	. . . . . . . . . . . 12 ⊢ ((((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
122	121	expl 457	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦))
123	120, 122	impbid 212	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
124	42, 123	bitr3id 285	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
125	124, 44	bitr4di 289	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
126	93, 99, 100, 101, 30, 36, 125	eqrelrd2 32676	. . . . . . 7 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
127	86, 88, 89, 126	syl21anc 838	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
128	80, 127	jca 511	. . . . 5 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
129	68, 128	impbii 209	. . . 4 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
130	129	a1i 11	. . 3 ⊢ (⊤ → ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))))
131	1, 8, 10, 130	f1od 7612	. 2 ⊢ (⊤ → 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵))
132	131	mptru 1549	1 ⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114  {cab 2715  {crab 3400  Vcvv 3441   ⊆ wss 3902  𝒫 cpw 4555  ⟨cop 4587   class class class wbr 5099  {copab 5161   ↦ cmpt 5180   × cxp 5623  dom cdm 5625  Rel wrel 5630  ⟶wf 6489  –1-1-onto→wf1o 6492  ‘cfv 6493  (class class class)co 7360   ↑_m cmap 8767

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-map 8769

This theorem is referenced by:  fpwrelmapffs  32794