rfovcnvf1od - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rfovcnvf1od		Structured version Visualization version GIF version

Theorem rfovcnvf1od 42740

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 2732	. . 3 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
2		rfovd.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		ssrab2 4076	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵
4	3	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵)
5	2, 4	sselpwd 5325	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
6	5	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵)
7	6	fmpttd 7111	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
8	2	pwexd 5376	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
9		rfovd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
10	8, 9	elmapd 8830	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑_m 𝐴) ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
11	7, 10	mpbird 256	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑_m 𝐴))
12	11	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑_m 𝐴))
13	9, 2	xpexd 7734	. . . . 5 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
14	13	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → (𝐴 × 𝐵) ∈ V)
15	8, 9	elmapd 8830	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
16	15	biimpa 477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
17	16	ffvelcdmda 7083	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵)
18	17	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝒫 𝐵))
19		elpwi 4608	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑓‘𝑥) ⊆ 𝐵)
20	19	sseld 3980	. . . . . . . . 9 ⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))
21	18, 20	syl6 35	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)))
22	21	imdistand 571	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
23		trud 1551	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ⊤)
24	22, 23	jca2 514	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)))
25	24	ssopab2dv 5550	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)})
26		opabssxp 5766	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
27	25, 26	sstrdi 3993	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ (𝐴 × 𝐵))
28	14, 27	sselpwd 5325	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29		simplrr 776	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))
30		elmapfn 8855	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝑓 Fn 𝐴)
31	29, 30	syl 17	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 Fn 𝐴)
32	2	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝐵 ∈ 𝑊)
33		rabexg 5330	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
34	33	ralrimivw 3150	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V)
35		nfcv 2903	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
36	35	fnmptf 6683	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
37	32, 34, 36	3syl 18	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴)
38		dfin5 3955	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)}
39		simpllr 774	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)))
40		elmapi 8839	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
41	39, 40	simpl2im 504	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
43	41, 42	ffvelcdmd 7084	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
44	43	elpwid 4610	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
45		sseqin2 4214	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
46	44, 45	sylib 217	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
47		ibar 529	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐴 → (𝑏 ∈ (𝑓‘𝑢) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
48	47	rabbidv 3440	. . . . . . . 8 ⊢ (𝑢 ∈ 𝐴 → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
49	48	adantl 482	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
50	38, 46, 49	3eqtr3a 2796	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
51		breq2 5151	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (𝑥𝑟𝑦 ↔ 𝑥𝑟𝑏))
52	51	cbvrabv 3442	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏}
53		breq1 5150	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ 𝑎𝑟𝑏))
54		df-br 5148	. . . . . . . . . . 11 ⊢ (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
55	53, 54	bitrdi 286	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
56	55	rabbidv 3440	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
57	52, 56	eqtrid 2784	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
58	57	cbvmptv 5260	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59		simpr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
60	59	opeq1d 4878	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61		simpllr 774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
62	60, 61	eleq12d 2827	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
63		vex 3478	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
64		vex 3478	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
65		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑥 = 𝑢)
66	65	eleq1d 2818	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
67		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑦 = 𝑏)
68	65	fveq2d 6892	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑓‘𝑥) = (𝑓‘𝑢))
69	67, 68	eleq12d 2827	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑏 ∈ (𝑓‘𝑢)))
70	66, 69	anbi12d 631	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
71	63, 64, 70	opelopaba 5535	. . . . . . . . 9 ⊢ (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))
72	62, 71	bitrdi 286	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))))
73	72	rabbidv 3440	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
74	2	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝐵 ∈ 𝑊)
75		rabexg 5330	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
76	74, 75	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V)
77	58, 73, 42, 76	fvmptd2 7003	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))})
78	50, 77	eqtr4d 2775	. . . . 5 ⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢))
79	31, 37, 78	eqfnfvd 7032	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
80		simplrl 775	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
81	80	elpwid 4610	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82		xpss 5691	. . . . . . 7 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
83	81, 82	sstrdi 3993	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84		df-rel 5682	. . . . . 6 ⊢ (Rel 𝑟 ↔ 𝑟 ⊆ (V × V))
85	83, 84	sylibr 233	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟)
86		relopabv 5819	. . . . . 6 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}
87	86	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
88		simpl 483	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
89	2, 88	anim12i 613	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) → (𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
90	89	anim1i 615	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
91		vex 3478	. . . . . . . 8 ⊢ 𝑣 ∈ V
92		simpl 483	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
93	92	eleq1d 2818	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
94		simpr 485	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
95	92	fveq2d 6892	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑓‘𝑥) = (𝑓‘𝑢))
96	94, 95	eleq12d 2827	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
97	93, 96	anbi12d 631	. . . . . . . 8 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))))
98	63, 91, 97	opelopaba 5535	. . . . . . 7 ⊢ (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)))
99		breq2 5151	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ 𝑢𝑟𝑣))
100		df-br 5148	. . . . . . . . . . . 12 ⊢ (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
101	99, 100	bitrdi 286	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102	101	elrab 3682	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103	102	anbi2i 623	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104	103	a1i 11	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105		simplr 767	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))
106		breq1 5150	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑦 ↔ 𝑎𝑟𝑦))
107	106	rabbidv 3440	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦})
108		breq2 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑎𝑟𝑦 ↔ 𝑎𝑟𝑏))
109	108	cbvrabv 3442	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}
110	107, 109	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
111	110	cbvmptv 5260	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})
112	105, 111	eqtrdi 2788	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}))
113		breq1 5150	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑢 → (𝑎𝑟𝑏 ↔ 𝑢𝑟𝑏))
114	113	rabbidv 3440	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑢 → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
115	114	adantl 482	. . . . . . . . . . 11 ⊢ (((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
116		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
117		rabexg 5330	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
118	117	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V)
119	112, 115, 116, 118	fvmptd 7002	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})
120	119	eleq2d 2819	. . . . . . . . 9 ⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}))
121	120	pm5.32da 579	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})))
122		simplr 767	. . . . . . . . . 10 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123	122	elpwid 4610	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
124	63, 91	opeldm 5905	. . . . . . . . . . . 12 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ dom 𝑟)
125		dmss 5900	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126		dmxpss 6167	. . . . . . . . . . . . . 14 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
127	125, 126	sstrdi 3993	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ 𝐴)
128	127	sseld 3980	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟 → 𝑢 ∈ 𝐴))
129	124, 128	syl5 34	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑢 ∈ 𝐴))
130	129	pm4.71rd 563	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
131	63, 91	opelrn 5940	. . . . . . . . . . . . 13 ⊢ (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ ran 𝑟)
132		rnss 5936	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133		rnxpss 6168	. . . . . . . . . . . . . . 15 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
134	132, 133	sstrdi 3993	. . . . . . . . . . . . . 14 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ 𝐵)
135	134	sseld 3980	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟 → 𝑣 ∈ 𝐵))
136	131, 135	syl5 34	. . . . . . . . . . . 12 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 → 𝑣 ∈ 𝐵))
137	136	pm4.71rd 563	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138	137	anbi2d 629	. . . . . . . . . 10 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢 ∈ 𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139	130, 138	bitrd 278	. . . . . . . . 9 ⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140	123, 139	syl 17	. . . . . . . 8 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141	104, 121, 140	3bitr4d 310	. . . . . . 7 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
142	98, 141	bitr2id 283	. . . . . 6 ⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
143	142	eqrelrdv2 5793	. . . . 5 ⊢ (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
144	85, 87, 90, 143	syl21anc 836	. . . 4 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})
145	79, 144	impbida 799	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
146	1, 12, 28, 145	f1ocnv2d 7655	. 2 ⊢ (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝐴) ∧ ^◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
147		rfovcnvf1od.f	. . . 4 ⊢ 𝐹 = (𝐴𝑂𝐵)
148		rfovd.rf	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))
149	148, 9, 2	rfovd 42737	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
150	147, 149	eqtrid 2784	. . 3 ⊢ (𝜑 → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
151		f1oeq1 6818	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝐴)))
152		cnveq 5871	. . . . 5 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ^◡𝐹 = ^◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
153	152	eqeq1d 2734	. . . 4 ⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (^◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ ^◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
154	151, 153	anbi12d 631	. . 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 256	1 ⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝐴) ∧ ^◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ⊤wtru 1542 ∈ wcel 2106 ∀wral 3061 {crab 3432 Vcvv 3474 ∩ cin 3946 ⊆ wss 3947 𝒫 cpw 4601 ⟨cop 4633 class class class wbr 5147 {copab 5209 ↦ cmpt 5230 × cxp 5673 ^◡ccnv 5674 dom cdm 5675 ran crn 5676 Rel wrel 5680 Fn wfn 6535 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7405 ∈ cmpo 7407 ↑_m cmap 8816

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7971 df-2nd 7972 df-map 8818

This theorem is referenced by: rfovcnvd 42741 rfovf1od 42742

W3C validator