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

Theorem rfovcnvf1od 42266
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.
StepHypRef Expression
1 eqid 2736 . . 3 (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
2 rfovd.b . . . . . . . 8 (𝜑𝐵𝑊)
3 ssrab2 4037 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵
43a1i 11 . . . . . . . 8 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵)
52, 4sselpwd 5283 . . . . . . 7 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
65adantr 481 . . . . . 6 ((𝜑𝑥𝐴) → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76fmpttd 7063 . . . . 5 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
82pwexd 5334 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
9 rfovd.a . . . . . 6 (𝜑𝐴𝑉)
108, 9elmapd 8779 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴) ↔ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
117, 10mpbird 256 . . . 4 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴))
1211adantr 481 . . 3 ((𝜑𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴))
139, 2xpexd 7685 . . . . 5 (𝜑 → (𝐴 × 𝐵) ∈ V)
1413adantr 481 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝐴 × 𝐵) ∈ V)
158, 9elmapd 8779 . . . . . . . . . . . 12 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
1615biimpa 477 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
1716ffvelcdmda 7035 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 𝒫 𝐵)
1817ex 413 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝒫 𝐵))
19 elpwi 4567 . . . . . . . . . 10 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑓𝑥) ⊆ 𝐵)
2019sseld 3943 . . . . . . . . 9 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵))
2118, 20syl6 35 . . . . . . . 8 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑥𝐴 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵)))
2221imdistand 571 . . . . . . 7 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → (𝑥𝐴𝑦𝐵)))
23 trud 1551 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ⊤)
2422, 23jca2 514 . . . . . 6 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ((𝑥𝐴𝑦𝐵) ∧ ⊤)))
2524ssopab2dv 5508 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)})
26 opabssxp 5724 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
2725, 26sstrdi 3956 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ (𝐴 × 𝐵))
2814, 27sselpwd 5283 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29 simplrr 776 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 ∈ (𝒫 𝐵m 𝐴))
30 elmapfn 8803 . . . . . 6 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓 Fn 𝐴)
3129, 30syl 17 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 Fn 𝐴)
322ad2antrr 724 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝐵𝑊)
33 rabexg 5288 . . . . . . 7 (𝐵𝑊 → {𝑦𝐵𝑥𝑟𝑦} ∈ V)
3433ralrimivw 3147 . . . . . 6 (𝐵𝑊 → ∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V)
35 nfcv 2907 . . . . . . 7 𝑥𝐴
3635fnmptf 6637 . . . . . 6 (∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
3732, 34, 363syl 18 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
38 dfin5 3918 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑏𝐵𝑏 ∈ (𝑓𝑢)}
39 simpllr 774 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴)))
40 elmapi 8787 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
4139, 40simpl2im 504 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42 simpr 485 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑢𝐴)
4341, 42ffvelcdmd 7036 . . . . . . . . 9 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
4443elpwid 4569 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
45 sseqin2 4175 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
4644, 45sylib 217 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
47 ibar 529 . . . . . . . . 9 (𝑢𝐴 → (𝑏 ∈ (𝑓𝑢) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
4847rabbidv 3415 . . . . . . . 8 (𝑢𝐴 → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
4948adantl 482 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
5038, 46, 493eqtr3a 2800 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
51 breq2 5109 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑥𝑟𝑦𝑥𝑟𝑏))
5251cbvrabv 3417 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑥𝑟𝑏}
53 breq1 5108 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝑟𝑏𝑎𝑟𝑏))
54 df-br 5106 . . . . . . . . . . 11 (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
5553, 54bitrdi 286 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
5655rabbidv 3415 . . . . . . . . 9 (𝑥 = 𝑎 → {𝑏𝐵𝑥𝑟𝑏} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5752, 56eqtrid 2788 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5857cbvmptv 5218 . . . . . . 7 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59 simpr 485 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
6059opeq1d 4836 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61 simpllr 774 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
6260, 61eleq12d 2832 . . . . . . . . 9 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
63 vex 3449 . . . . . . . . . 10 𝑢 ∈ V
64 vex 3449 . . . . . . . . . 10 𝑏 ∈ V
65 simpl 483 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑥 = 𝑢)
6665eleq1d 2822 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑥𝐴𝑢𝐴))
67 simpr 485 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑦 = 𝑏)
6865fveq2d 6846 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑓𝑥) = (𝑓𝑢))
6967, 68eleq12d 2832 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑏 ∈ (𝑓𝑢)))
7066, 69anbi12d 631 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑏) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7163, 64, 70opelopaba 5493 . . . . . . . . 9 (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢)))
7262, 71bitrdi 286 . . . . . . . 8 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7372rabbidv 3415 . . . . . . 7 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
742ad3antrrr 728 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝐵𝑊)
75 rabexg 5288 . . . . . . . 8 (𝐵𝑊 → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7674, 75syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7758, 73, 42, 76fvmptd2 6956 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
7850, 77eqtr4d 2779 . . . . 5 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢))
7931, 37, 78eqfnfvd 6985 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
80 simplrl 775 . . . . . . . 8 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
8180elpwid 4569 . . . . . . 7 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82 xpss 5649 . . . . . . 7 (𝐴 × 𝐵) ⊆ (V × V)
8381, 82sstrdi 3956 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84 df-rel 5640 . . . . . 6 (Rel 𝑟𝑟 ⊆ (V × V))
8583, 84sylibr 233 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel 𝑟)
86 relopabv 5777 . . . . . 6 Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}
8786a1i 11 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
88 simpl 483 . . . . . . 7 ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
892, 88anim12i 613 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) → (𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
9089anim1i 615 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
91 vex 3449 . . . . . . . 8 𝑣 ∈ V
92 simpl 483 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
9392eleq1d 2822 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝐴𝑢𝐴))
94 simpr 485 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
9592fveq2d 6846 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑓𝑥) = (𝑓𝑢))
9694, 95eleq12d 2832 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
9793, 96anbi12d 631 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢))))
9863, 91, 97opelopaba 5493 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢)))
99 breq2 5109 . . . . . . . . . . . 12 (𝑏 = 𝑣 → (𝑢𝑟𝑏𝑢𝑟𝑣))
100 df-br 5106 . . . . . . . . . . . 12 (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
10199, 100bitrdi 286 . . . . . . . . . . 11 (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102101elrab 3645 . . . . . . . . . 10 (𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏} ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103102anbi2i 623 . . . . . . . . 9 ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104103a1i 11 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105 simplr 767 . . . . . . . . . . . 12 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
106 breq1 5108 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝑥𝑟𝑦𝑎𝑟𝑦))
107106rabbidv 3415 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑦𝐵𝑎𝑟𝑦})
108 breq2 5109 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (𝑎𝑟𝑦𝑎𝑟𝑏))
109108cbvrabv 3417 . . . . . . . . . . . . . 14 {𝑦𝐵𝑎𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏}
110107, 109eqtrdi 2792 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏})
111110cbvmptv 5218 . . . . . . . . . . . 12 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏})
112105, 111eqtrdi 2792 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏}))
113 breq1 5108 . . . . . . . . . . . . 13 (𝑎 = 𝑢 → (𝑎𝑟𝑏𝑢𝑟𝑏))
114113rabbidv 3415 . . . . . . . . . . . 12 (𝑎 = 𝑢 → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
115114adantl 482 . . . . . . . . . . 11 (((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
116 simpr 485 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑢𝐴)
117 rabexg 5288 . . . . . . . . . . . 12 (𝐵𝑊 → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
118117ad3antrrr 728 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
119112, 115, 116, 118fvmptd 6955 . . . . . . . . . 10 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵𝑢𝑟𝑏})
120119eleq2d 2823 . . . . . . . . 9 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑣 ∈ (𝑓𝑢) ↔ 𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}))
121120pm5.32da 579 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ (𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏})))
122 simplr 767 . . . . . . . . . 10 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123122elpwid 4569 . . . . . . . . 9 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
12463, 91opeldm 5863 . . . . . . . . . . . 12 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢 ∈ dom 𝑟)
125 dmss 5858 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126 dmxpss 6123 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐵) ⊆ 𝐴
127125, 126sstrdi 3956 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟𝐴)
128127sseld 3943 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟𝑢𝐴))
129124, 128syl5 34 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢𝐴))
130129pm4.71rd 563 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
13163, 91opelrn 5898 . . . . . . . . . . . . 13 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣 ∈ ran 𝑟)
132 rnss 5894 . . . . . . . . . . . . . . 15 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133 rnxpss 6124 . . . . . . . . . . . . . . 15 ran (𝐴 × 𝐵) ⊆ 𝐵
134132, 133sstrdi 3956 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟𝐵)
135134sseld 3943 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟𝑣𝐵))
136131, 135syl5 34 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣𝐵))
137136pm4.71rd 563 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138137anbi2d 629 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139130, 138bitrd 278 . . . . . . . . 9 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140123, 139syl 17 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141104, 121, 1403bitr4d 310 . . . . . . 7 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
14298, 141bitr2id 283 . . . . . 6 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
143142eqrelrdv2 5751 . . . . 5 (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14485, 87, 90, 143syl21anc 836 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14579, 144impbida 799 . . 3 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
1461, 12, 28, 145f1ocnv2d 7606 . 2 (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
147 rfovcnvf1od.f . . . 4 𝐹 = (𝐴𝑂𝐵)
148 rfovd.rf . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥𝑎 ↦ {𝑦𝑏𝑥𝑟𝑦})))
149148, 9, 2rfovd 42263 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
150147, 149eqtrid 2788 . . 3 (𝜑𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
151 f1oeq1 6772 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴)))
152 cnveq 5829 . . . . 5 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
153152eqeq1d 2738 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
154151, 153anbi12d 631 . . 3 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))))
155150, 154syl 17 . 2 (𝜑 → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))))
156146, 155mpbird 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 3064  {crab 3407  Vcvv 3445  cin 3909  wss 3910  𝒫 cpw 4560  cop 4592   class class class wbr 5105  {copab 5167  cmpt 5188   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  Rel wrel 5638   Fn wfn 6491  wf 6492  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  cmpo 7359  m cmap 8765
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767
This theorem is referenced by:  rfovcnvd  42267  rfovf1od  42268
  Copyright terms: Public domain W3C validator