fpwrelmap - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fpwrelmap		Structured version Visualization version GIF version

Theorem fpwrelmap 29508

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 9270 and marypha2lem1 8341. (Contributed by Thierry Arnoux, 28-Aug-2017.)

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

**Assertion**
Ref	Expression
fpwrelmap	⊢ 𝑀:(𝒫 𝐵 ↑_𝑚 𝐴)–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 ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
2		fpwrelmap.1	. . . . . 6 ⊢ 𝐴 ∈ V
3	2	a1i 11	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → 𝐴 ∈ V)
4		simpr 477	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ (𝑓‘𝑥))
5		elmapi 7879	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6	5	ffvelrnda 6359	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
7	6	adantr 481	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
8		elelpwi 4171	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ∈ 𝒫 𝐵) → 𝑦 ∈ 𝐵)
9	4, 7, 8	syl2anc 693	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
10	9	ex 450	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
11	10	alrimiv 1855	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
12		abss 3671	. . . . . . 7 ⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
13		fpwrelmap.2	. . . . . . . 8 ⊢ 𝐵 ∈ V
14	13	ssex 4802	. . . . . . 7 ⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
15	12, 14	sylbir 225	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
16	11, 15	syl 17	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
17	3, 16	opabex3d 7145	. . . 4 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
18	17	adantl 482	. . 3 ⊢ ((⊤ ∧ 𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
19	2	mptex 6486	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V
20	19	a1i 11	. . 3 ⊢ ((⊤ ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V)
21	10	imdistanda 729	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
22	21	ssopab2dv 5004	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
23	22	adantr 481	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
24		simpr 477	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
25		df-xp 5120	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
26	25	a1i 11	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
27	23, 24, 26	3sstr4d 3648	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ⊆ (𝐴 × 𝐵))
28		selpw 4165	. . . . . . 7 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↔ 𝑟 ⊆ (𝐴 × 𝐵))
29	27, 28	sylibr 224	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
30	5	feqmptd 6249	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
31	30	adantr 481	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
32		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴)
33		nfopab1 4719	. . . . . . . . . 10 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
34	33	nfeq2 2780	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
35	32, 34	nfan 1828	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
36		df-rab 2921	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}
37	36	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
38		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴)
39		nfopab2 4720	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
40	39	nfeq2 2780	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
41	38, 40	nfan 1828	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
42		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
43	41, 42	nfan 1828	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴)
44	9	adantllr 755	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
45		df-br 4654	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
46		eleq2 2690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
47		opabid 4982	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
48	46, 47	syl6bb 276	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
49	45, 48	syl5bb 272	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
50	49	ad2antlr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
51		elfvdm 6220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ dom 𝑓)
52	51	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ dom 𝑓)
53		fdm 6051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝐴⟶𝒫 𝐵 → dom 𝑓 = 𝐴)
54	5, 53	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → dom 𝑓 = 𝐴)
55	54	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → dom 𝑓 = 𝐴)
56	52, 55	eleqtrd 2703	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ 𝐴)
57	56	ex 450	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ 𝐴))
58	57	pm4.71rd 667	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
59	58	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
60	50, 59	bitr4d 271	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ 𝑦 ∈ (𝑓‘𝑥)))
61	60	biimpar 502	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
62	44, 61	jca 554	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
63	62	ex 450	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
64	60	biimpd 219	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 → 𝑦 ∈ (𝑓‘𝑥)))
65	64	adantld 483	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥)))
66	63, 65	impbid 202	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
67	43, 66	abbid 2740	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
68		abid2 2745	. . . . . . . . . 10 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥)
69	68	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥))
70	37, 67, 69	3eqtr2rd 2663	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
71	35, 70	mpteq2da 4743	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
72	31, 71	eqtrd 2656	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
73	29, 72	jca 554	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
74		ssrab2 3687	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
75	13	elpw2 4828	. . . . . . . . . . . 12 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵 ↔ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵)
76	74, 75	mpbir 221	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵
77	76	a1i 11	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
78		eqid 2622	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
79	77, 78	fmptd 6385	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
80	79	adantr 481	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
81		simpr 477	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
82	81	feq1d 6030	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓:𝐴⟶𝒫 𝐵 ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
83	80, 82	mpbird 247	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓:𝐴⟶𝒫 𝐵)
84	13	pwex 4848	. . . . . . . 8 ⊢ 𝒫 𝐵 ∈ V
85	84, 2	elmap 7886	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)
86	83, 85	sylibr 224	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴))
87		elpwi 4168	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → 𝑟 ⊆ (𝐴 × 𝐵))
88	87	adantr 481	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
89		xpss 5226	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
90	88, 89	syl6ss 3615	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
91		df-rel 5121	. . . . . . . 8 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
92	90, 91	sylibr 224	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
93		relopab 5247	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
94	93	a1i 11	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
95		id 22	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
96		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
97		nfmpt1 4747	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
98	97	nfeq2 2780	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
99	96, 98	nfan 1828	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
100		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
101	42	nfci 2754	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
102		nfrab1 3122	. . . . . . . . . . 11 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}
103	101, 102	nfmpt 4746	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
104	103	nfeq2 2780	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
105	100, 104	nfan 1828	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
106		nfcv 2764	. . . . . . . 8 ⊢ Ⅎ𝑥𝑟
107		nfcv 2764	. . . . . . . 8 ⊢ Ⅎ𝑦𝑟
108		brelg 29421	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
109	87, 108	sylan 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
110	109	adantlr 751	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
111	110	simpld 475	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥 ∈ 𝐴)
112	110	simprd 479	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ 𝐵)
113		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥𝑟𝑦)
114	81	fveq1d 6193	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓‘𝑥) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥))
115	13	rabex 4813	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V
116	78	fvmpt2 6291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
117	115, 116	mpan2 707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
118	114, 117	sylan9eq 2676	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
119	118	eleq2d 2687	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
120		rabid 3116	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
121	119, 120	syl6bb 276	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
122	111, 121	syldan 487	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
123	112, 113, 122	mpbir2and 957	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥))
124	111, 123	jca 554	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
125	124	ex 450	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
126	121	simplbda 654	. . . . . . . . . . . 12 ⊢ ((((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
127	126	expl 648	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦))
128	125, 127	impbid 202	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
129	45, 128	syl5bbr 274	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
130	129, 47	syl6bbr 278	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
131	99, 105, 106, 107, 33, 39, 130	eqrelrd2 29426	. . . . . . 7 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
132	92, 94, 95, 131	syl21anc 1325	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
133	86, 132	jca 554	. . . . 5 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
134	73, 133	impbii 199	. . . 4 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
135	134	a1i 11	. . 3 ⊢ (⊤ → ((𝑓 ∈ (𝒫 𝐵 ↑_𝑚 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))))
136	1, 18, 20, 135	f1od 6885	. 2 ⊢ (⊤ → 𝑀:(𝒫 𝐵 ↑_𝑚 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵))
137	136	trud 1493	1 ⊢ 𝑀:(𝒫 𝐵 ↑_𝑚 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∀wal 1481 = wceq 1483 ⊤wtru 1484 ∈ wcel 1990 {cab 2608 {crab 2916 Vcvv 3200 ⊆ wss 3574 𝒫 cpw 4158 ⟨cop 4183 class class class wbr 4653 {copab 4712 ↦ cmpt 4729 × cxp 5112 dom cdm 5114 Rel wrel 5119 ⟶wf 5884 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 ↑_𝑚 cmap 7857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-map 7859

This theorem is referenced by: fpwrelmapffs 29509

W3C validator