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 38798
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→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
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 2806 . . 3 (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
2 rfovd.b . . . . . . . 8 (𝜑𝐵𝑊)
3 ssrab2 3884 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵
43a1i 11 . . . . . . . 8 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵)
52, 4sselpwd 5002 . . . . . . 7 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
65adantr 468 . . . . . 6 ((𝜑𝑥𝐴) → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76fmpttd 6607 . . . . 5 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
82pwexd 5049 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
9 rfovd.a . . . . . 6 (𝜑𝐴𝑉)
108, 9elmapd 8106 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵𝑚 𝐴) ↔ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
117, 10mpbird 248 . . . 4 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵𝑚 𝐴))
1211adantr 468 . . 3 ((𝜑𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵𝑚 𝐴))
13 xpexg 7190 . . . . . 6 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
149, 2, 13syl2anc 575 . . . . 5 (𝜑 → (𝐴 × 𝐵) ∈ V)
1514adantr 468 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝐴 × 𝐵) ∈ V)
168, 9elmapd 8106 . . . . . . . . . . . 12 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
1716biimpa 464 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
1817ffvelrnda 6581 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 𝒫 𝐵)
1918ex 399 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝒫 𝐵))
20 elpwi 4361 . . . . . . . . . 10 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑓𝑥) ⊆ 𝐵)
2120sseld 3797 . . . . . . . . 9 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵))
2219, 21syl6 35 . . . . . . . 8 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑥𝐴 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵)))
2322imdistand 562 . . . . . . 7 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → (𝑥𝐴𝑦𝐵)))
24 trud 1648 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ⊤)
2523, 24jca2 505 . . . . . 6 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ((𝑥𝐴𝑦𝐵) ∧ ⊤)))
2625ssopab2dv 5199 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)})
27 opabssxp 5395 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
2826, 27syl6ss 3810 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ (𝐴 × 𝐵))
2915, 28sselpwd 5002 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
30 simplrr 787 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))
31 elmapfn 8115 . . . . . 6 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓 Fn 𝐴)
3230, 31syl 17 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 Fn 𝐴)
332ad2antrr 708 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝐵𝑊)
34 rabexg 5006 . . . . . . 7 (𝐵𝑊 → {𝑦𝐵𝑥𝑟𝑦} ∈ V)
3534ralrimivw 3155 . . . . . 6 (𝐵𝑊 → ∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V)
36 nfcv 2948 . . . . . . 7 𝑥𝐴
3736fnmptf 6227 . . . . . 6 (∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
3833, 35, 373syl 18 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
39 dfin5 3777 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑏𝐵𝑏 ∈ (𝑓𝑢)}
40 simpllr 784 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴)))
41 elmapi 8114 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
4240, 41simpl2im 493 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
43 simpr 473 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑢𝐴)
4442, 43ffvelrnd 6582 . . . . . . . . 9 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
4544elpwid 4363 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
46 sseqin2 4016 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
4745, 46sylib 209 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
48 ibar 520 . . . . . . . . 9 (𝑢𝐴 → (𝑏 ∈ (𝑓𝑢) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
4948rabbidv 3379 . . . . . . . 8 (𝑢𝐴 → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
5049adantl 469 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
5139, 47, 503eqtr3a 2864 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
52 breq2 4848 . . . . . . . . . . 11 (𝑦 = 𝑏 → (𝑥𝑟𝑦𝑥𝑟𝑏))
5352cbvrabv 3389 . . . . . . . . . 10 {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑥𝑟𝑏}
54 breq1 4847 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥𝑟𝑏𝑎𝑟𝑏))
55 df-br 4845 . . . . . . . . . . . 12 (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
5654, 55syl6bb 278 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
5756rabbidv 3379 . . . . . . . . . 10 (𝑥 = 𝑎 → {𝑏𝐵𝑥𝑟𝑏} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5853, 57syl5eq 2852 . . . . . . . . 9 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5958cbvmptv 4944 . . . . . . . 8 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
6059a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟}))
61 simpr 473 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
6261opeq1d 4601 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
63 simpllr 784 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
6462, 63eleq12d 2879 . . . . . . . . 9 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
65 vex 3394 . . . . . . . . . 10 𝑢 ∈ V
66 vex 3394 . . . . . . . . . 10 𝑏 ∈ V
67 simpl 470 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑥 = 𝑢)
6867eleq1d 2870 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑥𝐴𝑢𝐴))
69 simpr 473 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑦 = 𝑏)
7067fveq2d 6412 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑓𝑥) = (𝑓𝑢))
7169, 70eleq12d 2879 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑏 ∈ (𝑓𝑢)))
7268, 71anbi12d 618 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑏) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7365, 66, 72opelopaba 5186 . . . . . . . . 9 (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢)))
7464, 73syl6bb 278 . . . . . . . 8 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7574rabbidv 3379 . . . . . . 7 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
762ad3antrrr 712 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝐵𝑊)
77 rabexg 5006 . . . . . . . 8 (𝐵𝑊 → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7876, 77syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7960, 75, 43, 78fvmptd 6509 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
8051, 79eqtr4d 2843 . . . . 5 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢))
8132, 38, 80eqfnfvd 6536 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
82 simplrl 786 . . . . . . . 8 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
8382elpwid 4363 . . . . . . 7 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
84 xpss 5327 . . . . . . 7 (𝐴 × 𝐵) ⊆ (V × V)
8583, 84syl6ss 3810 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
86 df-rel 5318 . . . . . 6 (Rel 𝑟𝑟 ⊆ (V × V))
8785, 86sylibr 225 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel 𝑟)
88 relopab 5449 . . . . . 6 Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}
8988a1i 11 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
90 simpl 470 . . . . . . 7 ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
912, 90anim12i 602 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) → (𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
9291anim1i 604 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
93 vex 3394 . . . . . . . 8 𝑣 ∈ V
94 simpl 470 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
9594eleq1d 2870 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝐴𝑢𝐴))
96 simpr 473 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
9794fveq2d 6412 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑓𝑥) = (𝑓𝑢))
9896, 97eleq12d 2879 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
9995, 98anbi12d 618 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢))))
10065, 93, 99opelopaba 5186 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢)))
101 breq2 4848 . . . . . . . . . . . 12 (𝑏 = 𝑣 → (𝑢𝑟𝑏𝑢𝑟𝑣))
102 df-br 4845 . . . . . . . . . . . 12 (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
103101, 102syl6bb 278 . . . . . . . . . . 11 (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
104103elrab 3559 . . . . . . . . . 10 (𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏} ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
105104anbi2i 611 . . . . . . . . 9 ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
106105a1i 11 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
107 simplr 776 . . . . . . . . . . . 12 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
108 breq1 4847 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝑥𝑟𝑦𝑎𝑟𝑦))
109108rabbidv 3379 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑦𝐵𝑎𝑟𝑦})
110 breq2 4848 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (𝑎𝑟𝑦𝑎𝑟𝑏))
111110cbvrabv 3389 . . . . . . . . . . . . . 14 {𝑦𝐵𝑎𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏}
112109, 111syl6eq 2856 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏})
113112cbvmptv 4944 . . . . . . . . . . . 12 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏})
114107, 113syl6eq 2856 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏}))
115 breq1 4847 . . . . . . . . . . . . 13 (𝑎 = 𝑢 → (𝑎𝑟𝑏𝑢𝑟𝑏))
116115rabbidv 3379 . . . . . . . . . . . 12 (𝑎 = 𝑢 → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
117116adantl 469 . . . . . . . . . . 11 (((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
118 simpr 473 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑢𝐴)
119 rabexg 5006 . . . . . . . . . . . 12 (𝐵𝑊 → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
120119ad3antrrr 712 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
121114, 117, 118, 120fvmptd 6509 . . . . . . . . . 10 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵𝑢𝑟𝑏})
122121eleq2d 2871 . . . . . . . . 9 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑣 ∈ (𝑓𝑢) ↔ 𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}))
123122pm5.32da 570 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ (𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏})))
124 simplr 776 . . . . . . . . . 10 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
125124elpwid 4363 . . . . . . . . 9 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
12665, 93opeldm 5529 . . . . . . . . . . . 12 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢 ∈ dom 𝑟)
127 dmss 5524 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
128 dmxpss 5776 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐵) ⊆ 𝐴
129127, 128syl6ss 3810 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟𝐴)
130129sseld 3797 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟𝑢𝐴))
131126, 130syl5 34 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢𝐴))
132131pm4.71rd 554 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
13365, 93opelrn 5558 . . . . . . . . . . . . 13 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣 ∈ ran 𝑟)
134 rnss 5555 . . . . . . . . . . . . . . 15 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
135 rnxpss 5777 . . . . . . . . . . . . . . 15 ran (𝐴 × 𝐵) ⊆ 𝐵
136134, 135syl6ss 3810 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟𝐵)
137136sseld 3797 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟𝑣𝐵))
138133, 137syl5 34 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣𝐵))
139138pm4.71rd 554 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
140139anbi2d 616 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141132, 140bitrd 270 . . . . . . . . 9 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
142125, 141syl 17 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
143106, 123, 1423bitr4d 302 . . . . . . 7 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
144100, 143syl5rbb 275 . . . . . 6 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
145144eqrelrdv2 5421 . . . . 5 (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14687, 89, 92, 145syl21anc 857 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14781, 146impbida 826 . . 3 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
1481, 12, 29, 147f1ocnv2d 7116 . 2 (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
149 rfovcnvf1od.f . . . 4 𝐹 = (𝐴𝑂𝐵)
150 rfovd.rf . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥𝑎 ↦ {𝑦𝑏𝑥𝑟𝑦})))
151150, 9, 2rfovd 38795 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
152149, 151syl5eq 2852 . . 3 (𝜑𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
153 f1oeq1 6343 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴)))
154 cnveq 5497 . . . . 5 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
155154eqeq1d 2808 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
156153, 155anbi12d 618 . . 3 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))))
157152, 156syl 17 . 2 (𝜑 → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))))
158148, 157mpbird 248 1 (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wtru 1638  wcel 2156  wral 3096  {crab 3100  Vcvv 3391  cin 3768  wss 3769  𝒫 cpw 4351  cop 4376   class class class wbr 4844  {copab 4906  cmpt 4923   × cxp 5309  ccnv 5310  dom cdm 5311  ran crn 5312  Rel wrel 5316   Fn wfn 6096  wf 6097  1-1-ontowf1o 6100  cfv 6101  (class class class)co 6874  cmpt2 6876  𝑚 cmap 8092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-1st 7398  df-2nd 7399  df-map 8094
This theorem is referenced by:  rfovcnvd  38799  rfovf1od  38800
  Copyright terms: Public domain W3C validator