Theorem rfovcnvf1od 44829

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 2762	. . 3 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
2		rfovd.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		ssrab2 4031	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
4	3	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵)
5	2, 4	sselpwd 5297	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
6	5	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
7	6	fmpttd 7111	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
8	2	pwexd 5348	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
9		rfovd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
10	8, 9	elmapd 8842	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴) ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
11	7, 10	mpbird 260	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴))
12	11	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑m 𝐴))
13	9, 2	xpexd 7753	. . . . 5 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
14	13	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V)
15	8, 9	elmapd 8842	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
16	15	biimpa 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
17	16	ffvelcdmda 7080	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
18	17	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝒫 𝐵))
19		elpwi 4567	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑓‘𝑥) ⊆ 𝐵)
20	19	sseld 3933	. . . . . . . . 9 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
21	18, 20	syl6 36	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)))
22	21	imdistand 581	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
23		trud 1580	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ⊤)
24	22, 23	jca2 523	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)))
25	24	ssopab2dv 5534	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)})
26		opabssxp 5751	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
27	25, 26	sstrdi 3946	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ (𝐴 × 𝐵))
28	14, 27	sselpwd 5297	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29		simplrr 790	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))
30		elmapfn 8869	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 Fn 𝐴)
31	29, 30	syl 18	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 Fn 𝐴)
32	2	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝐵 ∈ 𝑊)
33		rabexg 5306	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
34	33	ralrimivw 3160	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
35		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
36	35	fnmptf 6672	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
37	32, 34, 36	3syl 19	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
38		dfin5 3910	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)}
39		simpllr 788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)))
40		elmapi 8851	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
41	39, 40	simpl2im 513	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
43	41, 42	ffvelcdmd 7081	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
44	43	elpwid 4569	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
45		sseqin2 4172	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
46	44, 45	sylib 221	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
47		ibar 538	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐴 → (𝑏 ∈ (𝑓‘𝑢) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
48	47	rabbidv 3421	. . . . . . . 8 ⊢ (𝑢 ∈ 𝐴 → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
49	48	adantl 487	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
50	38, 46, 49	3eqtr3a 2821	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
51		breq2 5111	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (𝑥𝑟𝑦 ↔ 𝑥𝑟𝑏))
52	51	cbvrabv 3424	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏}
53		breq1 5110	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ 𝑎𝑟𝑏))
54		df-br 5108	. . . . . . . . . . 11 ⊢ (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
55	53, 54	bitrdi 290	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
56	55	rabbidv 3421	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
57	52, 56	eqtrid 2809	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
58	57	cbvmptv 5213	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
60	59	opeq1d 4842	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61		simpllr 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
62	60, 61	eleq12d 2856	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
63		vex 3457	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
64		vex 3457	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
65		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑥 = 𝑢)
66	65	eleq1d 2847	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
67		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑦 = 𝑏)
68	65	fveq2d 6886	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑓‘𝑥) = (𝑓‘𝑢))
69	67, 68	eleq12d 2856	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑏 ∈ (𝑓‘𝑢)))
70	66, 69	anbi12d 644	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
71	63, 64, 70	opelopaba 5518	. . . . . . . . 9 ⊢ (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))
72	62, 71	bitrdi 290	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
73	72	rabbidv 3421	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
74	2	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝐵 ∈ 𝑊)
75		rabexg 5306	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
76	74, 75	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
77	58, 73, 42, 76	fvmptd2 6999	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
78	50, 77	eqtr4d 2800	. . . . 5 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢))
79	31, 37, 78	eqfnfvd 7029	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
80		simplrl 789	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
81	80	elpwid 4569	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82		xpss 5675	. . . . . . 7 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
83	81, 82	sstrdi 3946	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84		df-rel 5666	. . . . . 6 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
85	83, 84	sylibr 237	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
86		relopabv 5806	. . . . . 6 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
87	86	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
88		simpl 488	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
89	2, 88	anim12i 625	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) → (𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
90	89	anim1i 627	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
91		vex 3457	. . . . . . . 8 ⊢ 𝑣 ∈ V
92		simpl 488	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
93	92	eleq1d 2847	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
94		simpr 490	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
95	92	fveq2d 6886	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑓‘𝑥) = (𝑓‘𝑢))
96	94, 95	eleq12d 2856	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
97	93, 96	anbi12d 644	. . . . . . . 8 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))))
98	63, 91, 97	opelopaba 5518	. . . . . . 7 ⊢ (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)))
99		breq2 5111	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ 𝑢𝑟𝑣))
100		df-br 5108	. . . . . . . . . . . 12 ⊢ (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
101	99, 100	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102	101	elrab 3648	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103	102	anbi2i 635	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104	103	a1i 11	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105		simplr 781	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
106		breq1 5110	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑦 ↔ 𝑎𝑟𝑦))
107	106	rabbidv 3421	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦})
108		breq2 5111	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑎𝑟𝑦 ↔ 𝑎𝑟𝑏))
109	108	cbvrabv 3424	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}
110	107, 109	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
111	110	cbvmptv 5213	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
112	105, 111	eqtrdi 2813	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}))
113		breq1 5110	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑢 → (𝑎𝑟𝑏 ↔ 𝑢𝑟𝑏))
114	113	rabbidv 3421	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑢 → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
115	114	adantl 487	. . . . . . . . . . 11 ⊢ (((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
116		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
117		rabexg 5306	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
118	117	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
119	112, 115, 116, 118	fvmptd 6998	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
120	119	eleq2d 2848	. . . . . . . . 9 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}))
121	120	pm5.32da 590	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})))
122		simplr 781	. . . . . . . . . 10 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123	122	elpwid 4569	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
124	63, 91	opeldm 5895	. . . . . . . . . . . 12 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ dom 𝑟)
125		dmss 5890	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126		dmxpss 6168	. . . . . . . . . . . . . 14 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
127	125, 126	sstrdi 3946	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ 𝐴)
128	127	sseld 3933	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟 → 𝑢 ∈ 𝐴))
129	124, 128	syl5 35	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ 𝐴))
130	129	pm4.71rd 572	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
131	63, 91	opelrn 5931	. . . . . . . . . . . . 13 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ ran 𝑟)
132		rnss 5927	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133		rnxpss 6169	. . . . . . . . . . . . . . 15 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
134	132, 133	sstrdi 3946	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ 𝐵)
135	134	sseld 3933	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟 → 𝑣 ∈ 𝐵))
136	131, 135	syl5 35	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ 𝐵))
137	136	pm4.71rd 572	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138	137	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139	130, 138	bitrd 282	. . . . . . . . 9 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140	123, 139	syl 18	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141	104, 121, 140	3bitr4d 314	. . . . . . 7 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
142	98, 141	bitr2id 287	. . . . . 6 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
143	142	eqrelrdv2 5779	. . . . 5 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
144	85, 87, 90, 143	syl21anc 851	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
145	79, 144	impbida 813	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
146	1, 12, 28, 145	f1ocnv2d 7670	. 2 ⊢ (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
147		rfovcnvf1od.f	. . . 4 ⊢ 𝐹 = (𝐴𝑂𝐵)
148		rfovd.rf	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))
149	148, 9, 2	rfovd 44826	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
150	147, 149	eqtrid 2809	. . 3 ⊢ (𝜑 → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
151		f1oeq1 6809	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴)))
152		cnveq 5857	. . . . 5 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ◡𝐹 = ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
153	152	eqeq1d 2764	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
154	151, 153	anbi12d 644	. . 3 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))))
155	150, 154	syl 18	. 2 ⊢ (𝜑 → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))))
156	146, 155	mpbird 260	1 ⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  ∀wral 3078  {crab 3414  Vcvv 3453   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4560  ⟨cop 4593   class class class wbr 5107  {copab 5171   ↦ cmpt 5190   × cxp 5657  ^◡ccnv 5658  dom cdm 5659  ran crn 5660  Rel wrel 5664   Fn wfn 6532  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7416   ∈ cmpo 7418   ↑_m cmap 8829

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7989  df-2nd 7990  df-map 8831

This theorem is used by:  rfovcnvd  44830  rfovf1od  44831