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 32499

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 10463 and marypha2lem1 9450. (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 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝐴 ∈ V)
4		simpr 484	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ (𝑓‘𝑥))
5		elmapi 8859	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6	5	ffvelcdmda 7088	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
7	6	adantr 480	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
8		elelpwi 4608	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ∈ 𝒫 𝐵) → 𝑦 ∈ 𝐵)
9	4, 7, 8	syl2anc 583	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
10	9	ex 412	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
11	10	alrimiv 1923	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
12		abss 4053	. . . . . . 7 ⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
13		fpwrelmap.2	. . . . . . . 8 ⊢ 𝐵 ∈ V
14	13	ssex 5315	. . . . . . 7 ⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
15	12, 14	sylbir 234	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
16	11, 15	syl 17	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
17	3, 16	opabex3d 7963	. . . 4 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
18	17	adantl 481	. . 3 ⊢ ((⊤ ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
19	2	mptex 7229	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V
20	19	a1i 11	. . 3 ⊢ ((⊤ ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V)
21	10	imdistanda 571	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
22	21	ssopab2dv 5547	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
24		simpr 484	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
25		df-xp 5678	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
26	25	a1i 11	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
27	23, 24, 26	3sstr4d 4025	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ⊆ (𝐴 × 𝐵))
28		velpw 4603	. . . . . . 7 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↔ 𝑟 ⊆ (𝐴 × 𝐵))
29	27, 28	sylibr 233	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
30	5	feqmptd 6961	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
31	30	adantr 480	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
32		nfv 1910	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)
33		nfopab1 5212	. . . . . . . . . 10 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
34	33	nfeq2 2915	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
35	32, 34	nfan 1895	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
36		df-rab 3428	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}
37	36	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
38		nfv 1910	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)
39		nfopab2 5213	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
40	39	nfeq2 2915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
41	38, 40	nfan 1895	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
42		nfv 1910	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
43	41, 42	nfan 1895	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴)
44	9	adantllr 718	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
45		df-br 5143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
46		eleq2 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
47		opabidw 5520	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
48	46, 47	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
49	45, 48	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
50	49	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
51		elfvdm 6928	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ dom 𝑓)
52	51	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ dom 𝑓)
53	5	fdmd 6727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → dom 𝑓 = 𝐴)
54	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → dom 𝑓 = 𝐴)
55	52, 54	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ 𝐴)
56	55	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ 𝐴))
57	56	pm4.71rd 562	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
58	57	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
59	50, 58	bitr4d 282	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ 𝑦 ∈ (𝑓‘𝑥)))
60	59	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
61	44, 60	jca 511	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
62	61	ex 412	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
63	59	biimpd 228	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 → 𝑦 ∈ (𝑓‘𝑥)))
64	63	adantld 490	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥)))
65	62, 64	impbid 211	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
66	43, 65	abbid 2798	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
67		abid2 2866	. . . . . . . . . 10 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥)
68	67	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥))
69	37, 66, 68	3eqtr2rd 2774	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
70	35, 69	mpteq2da 5240	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
71	31, 70	eqtrd 2767	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
72	29, 71	jca 511	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
73		ssrab2 4073	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
74	13, 73	elpwi2 5342	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵
75	74	a1i 11	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76	75	fmpttd 7119	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
77	76	adantr 480	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
78		simpr 484	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
79	78	feq1d 6701	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓:𝐴⟶𝒫 𝐵 ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
80	77, 79	mpbird 257	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓:𝐴⟶𝒫 𝐵)
81	13	pwex 5374	. . . . . . . 8 ⊢ 𝒫 𝐵 ∈ V
82	81, 2	elmap 8881	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)
83	80, 82	sylibr 233	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))
84		elpwi 4605	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → 𝑟 ⊆ (𝐴 × 𝐵))
85	84	adantr 480	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
86		xpss 5688	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
87	85, 86	sstrdi 3990	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
88		df-rel 5679	. . . . . . . 8 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
89	87, 88	sylibr 233	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
90		relopabv 5817	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
91	90	a1i 11	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
92		id 22	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
93		nfv 1910	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
94		nfmpt1 5250	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
95	94	nfeq2 2915	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
96	93, 95	nfan 1895	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
97		nfv 1910	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
98	42	nfci 2881	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
99		nfrab1 3446	. . . . . . . . . . 11 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}
100	98, 99	nfmpt 5249	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
101	100	nfeq2 2915	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
102	97, 101	nfan 1895	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
103		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑥𝑟
104		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑦𝑟
105		brelg 32382	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
106	84, 105	sylan 579	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
107	106	adantlr 714	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
108	107	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥 ∈ 𝐴)
109	107	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ 𝐵)
110		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥𝑟𝑦)
111	78	fveq1d 6893	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓‘𝑥) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥))
112	13	rabex 5328	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V
113		eqid 2727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
114	113	fvmpt2 7010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
115	112, 114	mpan2 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
116	111, 115	sylan9eq 2787	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
117	116	eleq2d 2814	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
118		rabid 3447	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
119	117, 118	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
120	108, 119	syldan 590	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
121	109, 110, 120	mpbir2and 712	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥))
122	108, 121	jca 511	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
123	122	ex 412	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
124	119	simplbda 499	. . . . . . . . . . . 12 ⊢ ((((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
125	124	expl 457	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦))
126	123, 125	impbid 211	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
127	45, 126	bitr3id 285	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
128	127, 47	bitr4di 289	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
129	96, 102, 103, 104, 33, 39, 128	eqrelrd2 32389	. . . . . . 7 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
130	89, 91, 92, 129	syl21anc 837	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
131	83, 130	jca 511	. . . . 5 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
132	72, 131	impbii 208	. . . 4 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
133	132	a1i 11	. . 3 ⊢ (⊤ → ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))))
134	1, 18, 20, 133	f1od 7667	. 2 ⊢ (⊤ → 𝑀:(𝒫 𝐵 ↑_m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵))
135	134	mptru 1541	1 ⊢ 𝑀:(𝒫 𝐵 ↑_m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∀wal 1532 = wceq 1534 ⊤wtru 1535 ∈ wcel 2099 {cab 2704 {crab 3427 Vcvv 3469 ⊆ wss 3944 𝒫 cpw 4598 ⟨cop 4630 class class class wbr 5142 {copab 5204 ↦ cmpt 5225 × cxp 5670 dom cdm 5672 Rel wrel 5677 ⟶wf 6538 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7414 ↑_m cmap 8836

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-ral 3057 df-rex 3066 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7417 df-oprab 7418 df-mpo 7419 df-1st 7987 df-2nd 7988 df-map 8838

This theorem is referenced by: fpwrelmapffs 32500

W3C validator