Theorem rfovcnvf1od 41241

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 2734	. . 3 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
2		rfovd.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		ssrab2 3983	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
4	3	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵)
5	2, 4	sselpwd 5208	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
6	5	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
7	6	fmpttd 6921	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
8	2	pwexd 5261	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
9		rfovd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
10	8, 9	elmapd 8511	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴) ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
11	7, 10	mpbird 260	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴))
12	11	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴))
13	9, 2	xpexd 7525	. . . . 5 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
14	13	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V)
15	8, 9	elmapd 8511	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
16	15	biimpa 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
17	16	ffvelrnda 6893	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
18	17	ex 416	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝒫 𝐵))
19		elpwi 4512	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑓‘𝑥) ⊆ 𝐵)
20	19	sseld 3890	. . . . . . . . 9 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
21	18, 20	syl6 35	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)))
22	21	imdistand 574	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
23		trud 1553	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ⊤)
24	22, 23	jca2 517	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)))
25	24	ssopab2dv 5421	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)})
26		opabssxp 5629	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
27	25, 26	sstrdi 3903	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ (𝐴 × 𝐵))
28	14, 27	sselpwd 5208	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29		simplrr 778	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))
30		elmapfn 8535	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 Fn 𝐴)
31	29, 30	syl 17	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 Fn 𝐴)
32	2	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝐵 ∈ 𝑊)
33		rabexg 5213	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
34	33	ralrimivw 3099	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
35		nfcv 2900	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
36	35	fnmptf 6503	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
37	32, 34, 36	3syl 18	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
38		dfin5 3865	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)}
39		simpllr 776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)))
40		elmapi 8519	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
41	39, 40	simpl2im 507	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42		simpr 488	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
43	41, 42	ffvelrnd 6894	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
44	43	elpwid 4514	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
45		sseqin2 4120	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
46	44, 45	sylib 221	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
47		ibar 532	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐴 → (𝑏 ∈ (𝑓‘𝑢) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
48	47	rabbidv 3383	. . . . . . . 8 ⊢ (𝑢 ∈ 𝐴 → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
49	48	adantl 485	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
50	38, 46, 49	3eqtr3a 2798	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
51		breq2 5047	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (𝑥𝑟𝑦 ↔ 𝑥𝑟𝑏))
52	51	cbvrabv 3395	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏}
53		breq1 5046	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ 𝑎𝑟𝑏))
54		df-br 5044	. . . . . . . . . . 11 ⊢ (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
55	53, 54	bitrdi 290	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
56	55	rabbidv 3383	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
57	52, 56	syl5eq 2786	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
58	57	cbvmptv 5147	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59		simpr 488	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
60	59	opeq1d 4780	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61		simpllr 776	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
62	60, 61	eleq12d 2828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
63		vex 3405	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
64		vex 3405	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
65		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑥 = 𝑢)
66	65	eleq1d 2818	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
67		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑦 = 𝑏)
68	65	fveq2d 6710	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑓‘𝑥) = (𝑓‘𝑢))
69	67, 68	eleq12d 2828	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑏 ∈ (𝑓‘𝑢)))
70	66, 69	anbi12d 634	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
71	63, 64, 70	opelopaba 5406	. . . . . . . . 9 ⊢ (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))
72	62, 71	bitrdi 290	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
73	72	rabbidv 3383	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
74	2	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝐵 ∈ 𝑊)
75		rabexg 5213	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
76	74, 75	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
77	58, 73, 42, 76	fvmptd2 6815	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
78	50, 77	eqtr4d 2777	. . . . 5 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢))
79	31, 37, 78	eqfnfvd 6844	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
80		simplrl 777	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
81	80	elpwid 4514	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82		xpss 5556	. . . . . . 7 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
83	81, 82	sstrdi 3903	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84		df-rel 5547	. . . . . 6 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
85	83, 84	sylibr 237	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
86		relopabv 5680	. . . . . 6 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
87	86	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
88		simpl 486	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
89	2, 88	anim12i 616	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) → (𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
90	89	anim1i 618	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
91		vex 3405	. . . . . . . 8 ⊢ 𝑣 ∈ V
92		simpl 486	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
93	92	eleq1d 2818	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
94		simpr 488	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
95	92	fveq2d 6710	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑓‘𝑥) = (𝑓‘𝑢))
96	94, 95	eleq12d 2828	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
97	93, 96	anbi12d 634	. . . . . . . 8 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))))
98	63, 91, 97	opelopaba 5406	. . . . . . 7 ⊢ (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)))
99		breq2 5047	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ 𝑢𝑟𝑣))
100		df-br 5044	. . . . . . . . . . . 12 ⊢ (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
101	99, 100	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102	101	elrab 3595	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103	102	anbi2i 626	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104	103	a1i 11	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105		simplr 769	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
106		breq1 5046	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑦 ↔ 𝑎𝑟𝑦))
107	106	rabbidv 3383	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦})
108		breq2 5047	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑎𝑟𝑦 ↔ 𝑎𝑟𝑏))
109	108	cbvrabv 3395	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}
110	107, 109	eqtrdi 2790	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
111	110	cbvmptv 5147	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
112	105, 111	eqtrdi 2790	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}))
113		breq1 5046	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑢 → (𝑎𝑟𝑏 ↔ 𝑢𝑟𝑏))
114	113	rabbidv 3383	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑢 → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
115	114	adantl 485	. . . . . . . . . . 11 ⊢ (((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
116		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
117		rabexg 5213	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
118	117	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
119	112, 115, 116, 118	fvmptd 6814	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
120	119	eleq2d 2819	. . . . . . . . 9 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}))
121	120	pm5.32da 582	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})))
122		simplr 769	. . . . . . . . . 10 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123	122	elpwid 4514	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
124	63, 91	opeldm 5765	. . . . . . . . . . . 12 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ dom 𝑟)
125		dmss 5760	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126		dmxpss 6023	. . . . . . . . . . . . . 14 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
127	125, 126	sstrdi 3903	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ 𝐴)
128	127	sseld 3890	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟 → 𝑢 ∈ 𝐴))
129	124, 128	syl5 34	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ 𝐴))
130	129	pm4.71rd 566	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
131	63, 91	opelrn 5801	. . . . . . . . . . . . 13 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ ran 𝑟)
132		rnss 5797	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133		rnxpss 6024	. . . . . . . . . . . . . . 15 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
134	132, 133	sstrdi 3903	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ 𝐵)
135	134	sseld 3890	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟 → 𝑣 ∈ 𝐵))
136	131, 135	syl5 34	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ 𝐵))
137	136	pm4.71rd 566	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138	137	anbi2d 632	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139	130, 138	bitrd 282	. . . . . . . . 9 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140	123, 139	syl 17	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141	104, 121, 140	3bitr4d 314	. . . . . . 7 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
142	98, 141	bitr2id 287	. . . . . 6 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
143	142	eqrelrdv2 5654	. . . . 5 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
144	85, 87, 90, 143	syl21anc 838	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
145	79, 144	impbida 801	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
146	1, 12, 28, 145	f1ocnv2d 7447	. 2 ⊢ (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
147		rfovcnvf1od.f	. . . 4 ⊢ 𝐹 = (𝐴𝑂𝐵)
148		rfovd.rf	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))
149	148, 9, 2	rfovd 41238	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
150	147, 149	syl5eq 2786	. . 3 ⊢ (𝜑 → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
151		f1oeq1 6638	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴)))
152		cnveq 5731	. . . . 5 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ◡𝐹 = ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
153	152	eqeq1d 2736	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
154	151, 153	anbi12d 634	. . 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 260	1 ⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ⊤wtru 1544   ∈ wcel 2110  ∀wral 3054  {crab 3058  Vcvv 3401   ∩ cin 3856   ⊆ wss 3857  𝒫 cpw 4503  ⟨cop 4537   class class class wbr 5043  {copab 5105   ↦ cmpt 5124   × cxp 5538  ^◡ccnv 5539  dom cdm 5540  ran crn 5541  Rel wrel 5545   Fn wfn 6364  ⟶wf 6365  –1-1-onto→wf1o 6368  ‘cfv 6369  (class class class)co 7202   ∈ cmpo 7204   ↑_m cmap 8497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-iun 4896  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-ov 7205  df-oprab 7206  df-mpo 7207  df-1st 7750  df-2nd 7751  df-map 8499

This theorem is referenced by:  rfovcnvd  41242  rfovf1od  41243