Theorem rfovcnvf1od 44000

Description: Properties of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵. (Contributed by RP, 27-Apr-2021.)

Hypotheses

Ref	Expression
rfovd.rf	⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))
rfovd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
rfovd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
rfovcnvf1od.f	⊢ 𝐹 = (𝐴𝑂𝐵)

Assertion

Ref	Expression
rfovcnvf1od	⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑟,𝑥,𝑦   𝐵,𝑎,𝑏,𝑓,𝑟,𝑥,𝑦   𝑊,𝑎,𝑥   𝜑,𝑎,𝑏,𝑓,𝑟,𝑥,𝑦

Allowed substitution hints:   𝐹(𝑥,𝑦,𝑓,𝑟,𝑎,𝑏)   𝑂(𝑥,𝑦,𝑓,𝑟,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑓,𝑟,𝑎,𝑏)   𝑊(𝑦,𝑓,𝑟,𝑏)

Proof of Theorem rfovcnvf1od

Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2730	. . 3 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
2		rfovd.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		ssrab2 4046	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
4	3	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵)
5	2, 4	sselpwd 5286	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
6	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
7	6	fmpttd 7090	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
8	2	pwexd 5337	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
9		rfovd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
10	8, 9	elmapd 8816	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴) ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
11	7, 10	mpbird 257	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴))
12	11	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴))
13	9, 2	xpexd 7730	. . . . 5 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
14	13	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V)
15	8, 9	elmapd 8816	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
16	15	biimpa 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
17	16	ffvelcdmda 7059	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
18	17	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝒫 𝐵))
19		elpwi 4573	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑓‘𝑥) ⊆ 𝐵)
20	19	sseld 3948	. . . . . . . . 9 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
21	18, 20	syl6 35	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)))
22	21	imdistand 570	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
23		trud 1550	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ⊤)
24	22, 23	jca2 513	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)))
25	24	ssopab2dv 5514	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)})
26		opabssxp 5734	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
27	25, 26	sstrdi 3962	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ (𝐴 × 𝐵))
28	14, 27	sselpwd 5286	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29		simplrr 777	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))
30		elmapfn 8841	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 Fn 𝐴)
31	29, 30	syl 17	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 Fn 𝐴)
32	2	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝐵 ∈ 𝑊)
33		rabexg 5295	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
34	33	ralrimivw 3130	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
35		nfcv 2892	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
36	35	fnmptf 6657	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
37	32, 34, 36	3syl 18	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
38		dfin5 3925	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)}
39		simpllr 775	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)))
40		elmapi 8825	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
41	39, 40	simpl2im 503	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
43	41, 42	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
44	43	elpwid 4575	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
45		sseqin2 4189	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
46	44, 45	sylib 218	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
47		ibar 528	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐴 → (𝑏 ∈ (𝑓‘𝑢) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
48	47	rabbidv 3416	. . . . . . . 8 ⊢ (𝑢 ∈ 𝐴 → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
49	48	adantl 481	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
50	38, 46, 49	3eqtr3a 2789	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
51		breq2 5114	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (𝑥𝑟𝑦 ↔ 𝑥𝑟𝑏))
52	51	cbvrabv 3419	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏}
53		breq1 5113	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ 𝑎𝑟𝑏))
54		df-br 5111	. . . . . . . . . . 11 ⊢ (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
55	53, 54	bitrdi 287	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
56	55	rabbidv 3416	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
57	52, 56	eqtrid 2777	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
58	57	cbvmptv 5214	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
60	59	opeq1d 4846	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
62	60, 61	eleq12d 2823	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
63		vex 3454	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
64		vex 3454	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
65		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑥 = 𝑢)
66	65	eleq1d 2814	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
67		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑦 = 𝑏)
68	65	fveq2d 6865	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑓‘𝑥) = (𝑓‘𝑢))
69	67, 68	eleq12d 2823	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑏 ∈ (𝑓‘𝑢)))
70	66, 69	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
71	63, 64, 70	opelopaba 5499	. . . . . . . . 9 ⊢ (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))
72	62, 71	bitrdi 287	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
73	72	rabbidv 3416	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
74	2	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝐵 ∈ 𝑊)
75		rabexg 5295	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
76	74, 75	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
77	58, 73, 42, 76	fvmptd2 6979	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
78	50, 77	eqtr4d 2768	. . . . 5 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢))
79	31, 37, 78	eqfnfvd 7009	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
80		simplrl 776	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
81	80	elpwid 4575	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82		xpss 5657	. . . . . . 7 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
83	81, 82	sstrdi 3962	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84		df-rel 5648	. . . . . 6 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
85	83, 84	sylibr 234	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
86		relopabv 5787	. . . . . 6 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
87	86	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
88		simpl 482	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
89	2, 88	anim12i 613	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) → (𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
90	89	anim1i 615	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
91		vex 3454	. . . . . . . 8 ⊢ 𝑣 ∈ V
92		simpl 482	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
93	92	eleq1d 2814	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
94		simpr 484	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
95	92	fveq2d 6865	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑓‘𝑥) = (𝑓‘𝑢))
96	94, 95	eleq12d 2823	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
97	93, 96	anbi12d 632	. . . . . . . 8 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))))
98	63, 91, 97	opelopaba 5499	. . . . . . 7 ⊢ (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)))
99		breq2 5114	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ 𝑢𝑟𝑣))
100		df-br 5111	. . . . . . . . . . . 12 ⊢ (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
101	99, 100	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102	101	elrab 3662	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103	102	anbi2i 623	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104	103	a1i 11	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105		simplr 768	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
106		breq1 5113	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑦 ↔ 𝑎𝑟𝑦))
107	106	rabbidv 3416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦})
108		breq2 5114	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑎𝑟𝑦 ↔ 𝑎𝑟𝑏))
109	108	cbvrabv 3419	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}
110	107, 109	eqtrdi 2781	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
111	110	cbvmptv 5214	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
112	105, 111	eqtrdi 2781	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}))
113		breq1 5113	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑢 → (𝑎𝑟𝑏 ↔ 𝑢𝑟𝑏))
114	113	rabbidv 3416	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑢 → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
115	114	adantl 481	. . . . . . . . . . 11 ⊢ (((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
116		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
117		rabexg 5295	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
118	117	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
119	112, 115, 116, 118	fvmptd 6978	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
120	119	eleq2d 2815	. . . . . . . . 9 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}))
121	120	pm5.32da 579	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})))
122		simplr 768	. . . . . . . . . 10 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123	122	elpwid 4575	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
124	63, 91	opeldm 5874	. . . . . . . . . . . 12 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ dom 𝑟)
125		dmss 5869	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126		dmxpss 6147	. . . . . . . . . . . . . 14 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
127	125, 126	sstrdi 3962	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ 𝐴)
128	127	sseld 3948	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟 → 𝑢 ∈ 𝐴))
129	124, 128	syl5 34	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ 𝐴))
130	129	pm4.71rd 562	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
131	63, 91	opelrn 5910	. . . . . . . . . . . . 13 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ ran 𝑟)
132		rnss 5906	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133		rnxpss 6148	. . . . . . . . . . . . . . 15 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
134	132, 133	sstrdi 3962	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ 𝐵)
135	134	sseld 3948	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟 → 𝑣 ∈ 𝐵))
136	131, 135	syl5 34	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ 𝐵))
137	136	pm4.71rd 562	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138	137	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139	130, 138	bitrd 279	. . . . . . . . 9 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140	123, 139	syl 17	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141	104, 121, 140	3bitr4d 311	. . . . . . 7 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
142	98, 141	bitr2id 284	. . . . . 6 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
143	142	eqrelrdv2 5761	. . . . 5 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
144	85, 87, 90, 143	syl21anc 837	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
145	79, 144	impbida 800	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
146	1, 12, 28, 145	f1ocnv2d 7645	. 2 ⊢ (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
147		rfovcnvf1od.f	. . . 4 ⊢ 𝐹 = (𝐴𝑂𝐵)
148		rfovd.rf	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))
149	148, 9, 2	rfovd 43997	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
150	147, 149	eqtrid 2777	. . 3 ⊢ (𝜑 → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
151		f1oeq1 6791	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴)))
152		cnveq 5840	. . . . 5 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ◡𝐹 = ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
153	152	eqeq1d 2732	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
154	151, 153	anbi12d 632	. . 3 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))))
155	150, 154	syl 17	. 2 ⊢ (𝜑 → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))))
156	146, 155	mpbird 257	1 ⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109  ∀wral 3045  {crab 3408  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917  𝒫 cpw 4566  ⟨cop 4598   class class class wbr 5110  {copab 5172   ↦ cmpt 5191   × cxp 5639  ^◡ccnv 5640  dom cdm 5641  ran crn 5642  Rel wrel 5646   Fn wfn 6509  ⟶wf 6510  –1-1-onto→wf1o 6513  ‘cfv 6514  (class class class)co 7390   ∈ cmpo 7392   ↑_m cmap 8802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-map 8804

This theorem is referenced by:  rfovcnvd  44001  rfovf1od  44002