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 32576

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 10471 and marypha2lem1 9458. (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 483	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ (𝑓‘𝑥))
5		elmapi 8866	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6	5	ffvelcdmda 7091	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
7	6	adantr 479	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
8		elelpwi 4613	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ∈ 𝒫 𝐵) → 𝑦 ∈ 𝐵)
9	4, 7, 8	syl2anc 582	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
10	9	ex 411	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
11	10	alrimiv 1922	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
12		abss 4055	. . . . . . 7 ⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
13		fpwrelmap.2	. . . . . . . 8 ⊢ 𝐵 ∈ V
14	13	ssex 5321	. . . . . . 7 ⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
15	12, 14	sylbir 234	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
16	11, 15	syl 17	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V)
17	3, 16	opabex3d 7968	. . . 4 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
18	17	adantl 480	. . 3 ⊢ ((⊤ ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V)
19	2	mptex 7233	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V
20	19	a1i 11	. . 3 ⊢ ((⊤ ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V)
21	10	imdistanda 570	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
22	21	ssopab2dv 5552	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
23	22	adantr 479	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
24		simpr 483	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
25		df-xp 5683	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
26	25	a1i 11	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)})
27	23, 24, 26	3sstr4d 4025	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ⊆ (𝐴 × 𝐵))
28		velpw 4608	. . . . . . 7 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↔ 𝑟 ⊆ (𝐴 × 𝐵))
29	27, 28	sylibr 233	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
30	5	feqmptd 6964	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
31	30	adantr 479	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)))
32		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)
33		nfopab1 5218	. . . . . . . . . 10 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
34	33	nfeq2 2910	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
35	32, 34	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
36		df-rab 3420	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}
37	36	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
38		nfv 1909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)
39		nfopab2 5219	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
40	39	nfeq2 2910	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
41	38, 40	nfan 1894	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
42		nfv 1909	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
43	41, 42	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴)
44	9	adantllr 717	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵)
45		df-br 5149	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
46		eleq2 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
47		opabidw 5525	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
48	46, 47	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
49	45, 48	bitrid 282	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
50	49	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
51		elfvdm 6931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ dom 𝑓)
52	51	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ dom 𝑓)
53	5	fdmd 6731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → dom 𝑓 = 𝐴)
54	53	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → dom 𝑓 = 𝐴)
55	52, 54	eleqtrd 2827	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ 𝐴)
56	55	ex 411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ 𝐴))
57	56	pm4.71rd 561	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
58	57	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
59	50, 58	bitr4d 281	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ 𝑦 ∈ (𝑓‘𝑥)))
60	59	biimpar 476	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
61	44, 60	jca 510	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
62	61	ex 411	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
63	59	biimpd 228	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 → 𝑦 ∈ (𝑓‘𝑥)))
64	63	adantld 489	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥)))
65	62, 64	impbid 211	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
66	43, 65	abbid 2796	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)})
67		abid2 2863	. . . . . . . . . 10 ⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥)
68	67	a1i 11	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥))
69	37, 66, 68	3eqtr2rd 2772	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
70	35, 69	mpteq2da 5246	. . . . . . 7 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
71	31, 70	eqtrd 2765	. . . . . 6 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
72	29, 71	jca 510	. . . . 5 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
73		ssrab2 4074	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
74	13, 73	elpwi2 5348	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵
75	74	a1i 11	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76	75	fmpttd 7122	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
77	76	adantr 479	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
78		simpr 483	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
79	78	feq1d 6706	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓:𝐴⟶𝒫 𝐵 ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
80	77, 79	mpbird 256	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓:𝐴⟶𝒫 𝐵)
81	13	pwex 5379	. . . . . . . 8 ⊢ 𝒫 𝐵 ∈ V
82	81, 2	elmap 8888	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)
83	80, 82	sylibr 233	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))
84		elpwi 4610	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → 𝑟 ⊆ (𝐴 × 𝐵))
85	84	adantr 479	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
86		xpss 5693	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
87	85, 86	sstrdi 3990	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
88		df-rel 5684	. . . . . . . 8 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
89	87, 88	sylibr 233	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
90		relopabv 5822	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
91	90	a1i 11	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
92		id 22	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
93		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
94		nfmpt1 5256	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
95	94	nfeq2 2910	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
96	93, 95	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
97		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑟 ∈ 𝒫 (𝐴 × 𝐵)
98	42	nfci 2878	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
99		nfrab1 3439	. . . . . . . . . . 11 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}
100	98, 99	nfmpt 5255	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
101	100	nfeq2 2910	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
102	97, 101	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
103		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑥𝑟
104		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑦𝑟
105		brelg 32457	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
106	84, 105	sylan 578	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
107	106	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
108	107	simpld 493	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥 ∈ 𝐴)
109	107	simprd 494	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ 𝐵)
110		simpr 483	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥𝑟𝑦)
111	78	fveq1d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓‘𝑥) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥))
112	13	rabex 5334	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V
113		eqid 2725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
114	113	fvmpt2 7013	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
115	112, 114	mpan2 689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
116	111, 115	sylan9eq 2785	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})
117	116	eleq2d 2811	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
118		rabid 3440	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))
119	117, 118	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
120	108, 119	syldan 589	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)))
121	109, 110, 120	mpbir2and 711	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥))
122	108, 121	jca 510	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))
123	122	ex 411	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
124	119	simplbda 498	. . . . . . . . . . . 12 ⊢ ((((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)
125	124	expl 456	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦))
126	123, 125	impbid 211	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
127	45, 126	bitr3id 284	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))))
128	127, 47	bitr4di 288	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑥, 𝑦⟩ ∈ 𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
129	96, 102, 103, 104, 33, 39, 128	eqrelrd2 32464	. . . . . . 7 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
130	89, 91, 92, 129	syl21anc 836	. . . . . 6 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
131	83, 130	jca 510	. . . . 5 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
132	72, 131	impbii 208	. . . 4 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
133	132	a1i 11	. . 3 ⊢ (⊤ → ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))))
134	1, 18, 20, 133	f1od 7671	. 2 ⊢ (⊤ → 𝑀:(𝒫 𝐵 ↑_m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵))
135	134	mptru 1540	1 ⊢ 𝑀:(𝒫 𝐵 ↑_m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1531 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 {cab 2702 {crab 3419 Vcvv 3463 ⊆ wss 3945 𝒫 cpw 4603 ⟨cop 4635 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 × cxp 5675 dom cdm 5677 Rel wrel 5682 ⟶wf 6543 –1-1-onto→wf1o 6546 ‘cfv 6547 (class class class)co 7417 ↑_m cmap 8843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-ov 7420 df-oprab 7421 df-mpo 7422 df-1st 7992 df-2nd 7993 df-map 8845

This theorem is referenced by: fpwrelmapffs 32577

W3C validator