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

Theorem rfovcnvf1od 39742
 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 2772 . . 3 (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
2 rfovd.b . . . . . . . 8 (𝜑𝐵𝑊)
3 ssrab2 3940 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵
43a1i 11 . . . . . . . 8 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵)
52, 4sselpwd 5082 . . . . . . 7 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
65adantr 473 . . . . . 6 ((𝜑𝑥𝐴) → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76fmpttd 6700 . . . . 5 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
82pwexd 5129 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
9 rfovd.a . . . . . 6 (𝜑𝐴𝑉)
108, 9elmapd 8218 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵𝑚 𝐴) ↔ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
117, 10mpbird 249 . . . 4 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵𝑚 𝐴))
1211adantr 473 . . 3 ((𝜑𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵𝑚 𝐴))
139, 2xpexd 7289 . . . . 5 (𝜑 → (𝐴 × 𝐵) ∈ V)
1413adantr 473 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝐴 × 𝐵) ∈ V)
158, 9elmapd 8218 . . . . . . . . . . . 12 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
1615biimpa 469 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
1716ffvelrnda 6674 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 𝒫 𝐵)
1817ex 405 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝒫 𝐵))
19 elpwi 4426 . . . . . . . . . 10 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑓𝑥) ⊆ 𝐵)
2019sseld 3851 . . . . . . . . 9 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵))
2118, 20syl6 35 . . . . . . . 8 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑥𝐴 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵)))
2221imdistand 563 . . . . . . 7 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → (𝑥𝐴𝑦𝐵)))
23 trud 1517 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ⊤)
2422, 23jca2 506 . . . . . 6 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ((𝑥𝐴𝑦𝐵) ∧ ⊤)))
2524ssopab2dv 5286 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)})
26 opabssxp 5489 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
2725, 26syl6ss 3864 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ (𝐴 × 𝐵))
2814, 27sselpwd 5082 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29 simplrr 765 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))
30 elmapfn 8227 . . . . . 6 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓 Fn 𝐴)
3129, 30syl 17 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 Fn 𝐴)
322ad2antrr 713 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝐵𝑊)
33 rabexg 5086 . . . . . . 7 (𝐵𝑊 → {𝑦𝐵𝑥𝑟𝑦} ∈ V)
3433ralrimivw 3127 . . . . . 6 (𝐵𝑊 → ∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V)
35 nfcv 2926 . . . . . . 7 𝑥𝐴
3635fnmptf 6311 . . . . . 6 (∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
3732, 34, 363syl 18 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
38 dfin5 3831 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑏𝐵𝑏 ∈ (𝑓𝑢)}
39 simpllr 763 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴)))
40 elmapi 8226 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
4139, 40simpl2im 496 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42 simpr 477 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑢𝐴)
4341, 42ffvelrnd 6675 . . . . . . . . 9 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
4443elpwid 4428 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
45 sseqin2 4073 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
4644, 45sylib 210 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
47 ibar 521 . . . . . . . . 9 (𝑢𝐴 → (𝑏 ∈ (𝑓𝑢) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
4847rabbidv 3397 . . . . . . . 8 (𝑢𝐴 → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
4948adantl 474 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
5038, 46, 493eqtr3a 2832 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
51 breq2 4929 . . . . . . . . . . 11 (𝑦 = 𝑏 → (𝑥𝑟𝑦𝑥𝑟𝑏))
5251cbvrabv 3406 . . . . . . . . . 10 {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑥𝑟𝑏}
53 breq1 4928 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥𝑟𝑏𝑎𝑟𝑏))
54 df-br 4926 . . . . . . . . . . . 12 (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
5553, 54syl6bb 279 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
5655rabbidv 3397 . . . . . . . . . 10 (𝑥 = 𝑎 → {𝑏𝐵𝑥𝑟𝑏} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5752, 56syl5eq 2820 . . . . . . . . 9 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5857cbvmptv 5024 . . . . . . . 8 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5958a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟}))
60 simpr 477 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
6160opeq1d 4679 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
62 simpllr 763 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
6361, 62eleq12d 2854 . . . . . . . . 9 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
64 vex 3412 . . . . . . . . . 10 𝑢 ∈ V
65 vex 3412 . . . . . . . . . 10 𝑏 ∈ V
66 simpl 475 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑥 = 𝑢)
6766eleq1d 2844 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑥𝐴𝑢𝐴))
68 simpr 477 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑦 = 𝑏)
6966fveq2d 6500 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑓𝑥) = (𝑓𝑢))
7068, 69eleq12d 2854 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑏 ∈ (𝑓𝑢)))
7167, 70anbi12d 621 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑏) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7264, 65, 71opelopaba 5273 . . . . . . . . 9 (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢)))
7363, 72syl6bb 279 . . . . . . . 8 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7473rabbidv 3397 . . . . . . 7 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
752ad3antrrr 717 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝐵𝑊)
76 rabexg 5086 . . . . . . . 8 (𝐵𝑊 → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7775, 76syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7859, 74, 42, 77fvmptd 6599 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
7950, 78eqtr4d 2811 . . . . 5 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢))
8031, 37, 79eqfnfvd 6628 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
81 simplrl 764 . . . . . . . 8 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
8281elpwid 4428 . . . . . . 7 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
83 xpss 5419 . . . . . . 7 (𝐴 × 𝐵) ⊆ (V × V)
8482, 83syl6ss 3864 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
85 df-rel 5410 . . . . . 6 (Rel 𝑟𝑟 ⊆ (V × V))
8684, 85sylibr 226 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel 𝑟)
87 relopab 5542 . . . . . 6 Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}
8887a1i 11 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
89 simpl 475 . . . . . . 7 ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
902, 89anim12i 603 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) → (𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
9190anim1i 605 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
92 vex 3412 . . . . . . . 8 𝑣 ∈ V
93 simpl 475 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
9493eleq1d 2844 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝐴𝑢𝐴))
95 simpr 477 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
9693fveq2d 6500 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑓𝑥) = (𝑓𝑢))
9795, 96eleq12d 2854 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
9894, 97anbi12d 621 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢))))
9964, 92, 98opelopaba 5273 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢)))
100 breq2 4929 . . . . . . . . . . . 12 (𝑏 = 𝑣 → (𝑢𝑟𝑏𝑢𝑟𝑣))
101 df-br 4926 . . . . . . . . . . . 12 (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
102100, 101syl6bb 279 . . . . . . . . . . 11 (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103102elrab 3589 . . . . . . . . . 10 (𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏} ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
104103anbi2i 613 . . . . . . . . 9 ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
105104a1i 11 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
106 simplr 756 . . . . . . . . . . . 12 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
107 breq1 4928 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝑥𝑟𝑦𝑎𝑟𝑦))
108107rabbidv 3397 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑦𝐵𝑎𝑟𝑦})
109 breq2 4929 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (𝑎𝑟𝑦𝑎𝑟𝑏))
110109cbvrabv 3406 . . . . . . . . . . . . . 14 {𝑦𝐵𝑎𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏}
111108, 110syl6eq 2824 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏})
112111cbvmptv 5024 . . . . . . . . . . . 12 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏})
113106, 112syl6eq 2824 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏}))
114 breq1 4928 . . . . . . . . . . . . 13 (𝑎 = 𝑢 → (𝑎𝑟𝑏𝑢𝑟𝑏))
115114rabbidv 3397 . . . . . . . . . . . 12 (𝑎 = 𝑢 → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
116115adantl 474 . . . . . . . . . . 11 (((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
117 simpr 477 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑢𝐴)
118 rabexg 5086 . . . . . . . . . . . 12 (𝐵𝑊 → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
119118ad3antrrr 717 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
120113, 116, 117, 119fvmptd 6599 . . . . . . . . . 10 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵𝑢𝑟𝑏})
121120eleq2d 2845 . . . . . . . . 9 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑣 ∈ (𝑓𝑢) ↔ 𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}))
122121pm5.32da 571 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ (𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏})))
123 simplr 756 . . . . . . . . . 10 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
124123elpwid 4428 . . . . . . . . 9 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
12564, 92opeldm 5622 . . . . . . . . . . . 12 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢 ∈ dom 𝑟)
126 dmss 5617 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
127 dmxpss 5865 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐵) ⊆ 𝐴
128126, 127syl6ss 3864 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟𝐴)
129128sseld 3851 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟𝑢𝐴))
130125, 129syl5 34 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢𝐴))
131130pm4.71rd 555 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
13264, 92opelrn 5653 . . . . . . . . . . . . 13 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣 ∈ ran 𝑟)
133 rnss 5649 . . . . . . . . . . . . . . 15 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
134 rnxpss 5866 . . . . . . . . . . . . . . 15 ran (𝐴 × 𝐵) ⊆ 𝐵
135133, 134syl6ss 3864 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟𝐵)
136135sseld 3851 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟𝑣𝐵))
137132, 136syl5 34 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣𝐵))
138137pm4.71rd 555 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
139138anbi2d 619 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140131, 139bitrd 271 . . . . . . . . 9 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141124, 140syl 17 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
142105, 122, 1413bitr4d 303 . . . . . . 7 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
14399, 142syl5rbb 276 . . . . . 6 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
144143eqrelrdv2 5514 . . . . 5 (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14586, 88, 91, 144syl21anc 825 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14680, 145impbida 788 . . 3 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵𝑚 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
1471, 12, 28, 146f1ocnv2d 7214 . 2 (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
148 rfovcnvf1od.f . . . 4 𝐹 = (𝐴𝑂𝐵)
149 rfovd.rf . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥𝑎 ↦ {𝑦𝑏𝑥𝑟𝑦})))
150149, 9, 2rfovd 39739 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
151148, 150syl5eq 2820 . . 3 (𝜑𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
152 f1oeq1 6430 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴)))
153 cnveq 5590 . . . . 5 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
154153eqeq1d 2774 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
155152, 154anbi12d 621 . . 3 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))))
156151, 155syl 17 . 2 (𝜑 → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))))
157147, 156mpbird 249 1 (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵𝑚 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507  ⊤wtru 1508   ∈ wcel 2050  ∀wral 3082  {crab 3086  Vcvv 3409   ∩ cin 3822   ⊆ wss 3823  𝒫 cpw 4416  ⟨cop 4441   class class class wbr 4925  {copab 4987   ↦ cmpt 5004   × cxp 5401  ◡ccnv 5402  dom cdm 5403  ran crn 5404  Rel wrel 5408   Fn wfn 6180  ⟶wf 6181  –1-1-onto→wf1o 6184  ‘cfv 6185  (class class class)co 6974   ∈ cmpo 6976   ↑𝑚 cmap 8204 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-1st 7499  df-2nd 7500  df-map 8206 This theorem is referenced by:  rfovcnvd  39743  rfovf1od  39744
 Copyright terms: Public domain W3C validator