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

Theorem rfovcnvf1od 40702
 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 2801 . . 3 (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
2 rfovd.b . . . . . . . 8 (𝜑𝐵𝑊)
3 ssrab2 4010 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵
43a1i 11 . . . . . . . 8 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵)
52, 4sselpwd 5197 . . . . . . 7 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
65adantr 484 . . . . . 6 ((𝜑𝑥𝐴) → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76fmpttd 6860 . . . . 5 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
82pwexd 5248 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
9 rfovd.a . . . . . 6 (𝜑𝐴𝑉)
108, 9elmapd 8407 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴) ↔ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
117, 10mpbird 260 . . . 4 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴))
1211adantr 484 . . 3 ((𝜑𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴))
139, 2xpexd 7458 . . . . 5 (𝜑 → (𝐴 × 𝐵) ∈ V)
1413adantr 484 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝐴 × 𝐵) ∈ V)
158, 9elmapd 8407 . . . . . . . . . . . 12 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
1615biimpa 480 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
1716ffvelrnda 6832 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 𝒫 𝐵)
1817ex 416 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝒫 𝐵))
19 elpwi 4509 . . . . . . . . . 10 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑓𝑥) ⊆ 𝐵)
2019sseld 3917 . . . . . . . . 9 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵))
2118, 20syl6 35 . . . . . . . 8 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑥𝐴 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵)))
2221imdistand 574 . . . . . . 7 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → (𝑥𝐴𝑦𝐵)))
23 trud 1548 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ⊤)
2422, 23jca2 517 . . . . . 6 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ((𝑥𝐴𝑦𝐵) ∧ ⊤)))
2524ssopab2dv 5406 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)})
26 opabssxp 5611 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
2725, 26sstrdi 3930 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ (𝐴 × 𝐵))
2814, 27sselpwd 5197 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29 simplrr 777 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 ∈ (𝒫 𝐵m 𝐴))
30 elmapfn 8416 . . . . . 6 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓 Fn 𝐴)
3129, 30syl 17 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 Fn 𝐴)
322ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝐵𝑊)
33 rabexg 5201 . . . . . . 7 (𝐵𝑊 → {𝑦𝐵𝑥𝑟𝑦} ∈ V)
3433ralrimivw 3153 . . . . . 6 (𝐵𝑊 → ∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V)
35 nfcv 2958 . . . . . . 7 𝑥𝐴
3635fnmptf 6460 . . . . . 6 (∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
3732, 34, 363syl 18 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
38 dfin5 3892 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑏𝐵𝑏 ∈ (𝑓𝑢)}
39 simpllr 775 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴)))
40 elmapi 8415 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
4139, 40simpl2im 507 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42 simpr 488 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑢𝐴)
4341, 42ffvelrnd 6833 . . . . . . . . 9 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
4443elpwid 4511 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
45 sseqin2 4145 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
4644, 45sylib 221 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
47 ibar 532 . . . . . . . . 9 (𝑢𝐴 → (𝑏 ∈ (𝑓𝑢) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
4847rabbidv 3430 . . . . . . . 8 (𝑢𝐴 → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
4948adantl 485 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
5038, 46, 493eqtr3a 2860 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
51 breq2 5037 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑥𝑟𝑦𝑥𝑟𝑏))
5251cbvrabv 3442 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑥𝑟𝑏}
53 breq1 5036 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝑟𝑏𝑎𝑟𝑏))
54 df-br 5034 . . . . . . . . . . 11 (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
5553, 54syl6bb 290 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
5655rabbidv 3430 . . . . . . . . 9 (𝑥 = 𝑎 → {𝑏𝐵𝑥𝑟𝑏} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5752, 56syl5eq 2848 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5857cbvmptv 5136 . . . . . . 7 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59 simpr 488 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
6059opeq1d 4774 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61 simpllr 775 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
6260, 61eleq12d 2887 . . . . . . . . 9 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
63 vex 3447 . . . . . . . . . 10 𝑢 ∈ V
64 vex 3447 . . . . . . . . . 10 𝑏 ∈ V
65 simpl 486 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑥 = 𝑢)
6665eleq1d 2877 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑥𝐴𝑢𝐴))
67 simpr 488 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑦 = 𝑏)
6865fveq2d 6653 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑓𝑥) = (𝑓𝑢))
6967, 68eleq12d 2887 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑏 ∈ (𝑓𝑢)))
7066, 69anbi12d 633 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑏) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7163, 64, 70opelopaba 5391 . . . . . . . . 9 (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢)))
7262, 71syl6bb 290 . . . . . . . 8 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7372rabbidv 3430 . . . . . . 7 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
742ad3antrrr 729 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝐵𝑊)
75 rabexg 5201 . . . . . . . 8 (𝐵𝑊 → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7674, 75syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7758, 73, 42, 76fvmptd2 6757 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
7850, 77eqtr4d 2839 . . . . 5 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢))
7931, 37, 78eqfnfvd 6786 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
80 simplrl 776 . . . . . . . 8 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
8180elpwid 4511 . . . . . . 7 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82 xpss 5539 . . . . . . 7 (𝐴 × 𝐵) ⊆ (V × V)
8381, 82sstrdi 3930 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84 df-rel 5530 . . . . . 6 (Rel 𝑟𝑟 ⊆ (V × V))
8583, 84sylibr 237 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel 𝑟)
86 relopab 5664 . . . . . 6 Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}
8786a1i 11 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
88 simpl 486 . . . . . . 7 ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
892, 88anim12i 615 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) → (𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
9089anim1i 617 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
91 vex 3447 . . . . . . . 8 𝑣 ∈ V
92 simpl 486 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
9392eleq1d 2877 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝐴𝑢𝐴))
94 simpr 488 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
9592fveq2d 6653 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑓𝑥) = (𝑓𝑢))
9694, 95eleq12d 2887 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
9793, 96anbi12d 633 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢))))
9863, 91, 97opelopaba 5391 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢)))
99 breq2 5037 . . . . . . . . . . . 12 (𝑏 = 𝑣 → (𝑢𝑟𝑏𝑢𝑟𝑣))
100 df-br 5034 . . . . . . . . . . . 12 (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
10199, 100syl6bb 290 . . . . . . . . . . 11 (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102101elrab 3631 . . . . . . . . . 10 (𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏} ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103102anbi2i 625 . . . . . . . . 9 ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104103a1i 11 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105 simplr 768 . . . . . . . . . . . 12 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
106 breq1 5036 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝑥𝑟𝑦𝑎𝑟𝑦))
107106rabbidv 3430 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑦𝐵𝑎𝑟𝑦})
108 breq2 5037 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (𝑎𝑟𝑦𝑎𝑟𝑏))
109108cbvrabv 3442 . . . . . . . . . . . . . 14 {𝑦𝐵𝑎𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏}
110107, 109eqtrdi 2852 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏})
111110cbvmptv 5136 . . . . . . . . . . . 12 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏})
112105, 111eqtrdi 2852 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏}))
113 breq1 5036 . . . . . . . . . . . . 13 (𝑎 = 𝑢 → (𝑎𝑟𝑏𝑢𝑟𝑏))
114113rabbidv 3430 . . . . . . . . . . . 12 (𝑎 = 𝑢 → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
115114adantl 485 . . . . . . . . . . 11 (((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
116 simpr 488 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑢𝐴)
117 rabexg 5201 . . . . . . . . . . . 12 (𝐵𝑊 → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
118117ad3antrrr 729 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
119112, 115, 116, 118fvmptd 6756 . . . . . . . . . 10 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵𝑢𝑟𝑏})
120119eleq2d 2878 . . . . . . . . 9 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑣 ∈ (𝑓𝑢) ↔ 𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}))
121120pm5.32da 582 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ (𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏})))
122 simplr 768 . . . . . . . . . 10 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123122elpwid 4511 . . . . . . . . 9 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
12463, 91opeldm 5744 . . . . . . . . . . . 12 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢 ∈ dom 𝑟)
125 dmss 5739 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126 dmxpss 5999 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐵) ⊆ 𝐴
127125, 126sstrdi 3930 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟𝐴)
128127sseld 3917 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟𝑢𝐴))
129124, 128syl5 34 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢𝐴))
130129pm4.71rd 566 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
13163, 91opelrn 5781 . . . . . . . . . . . . 13 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣 ∈ ran 𝑟)
132 rnss 5777 . . . . . . . . . . . . . . 15 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133 rnxpss 6000 . . . . . . . . . . . . . . 15 ran (𝐴 × 𝐵) ⊆ 𝐵
134132, 133sstrdi 3930 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟𝐵)
135134sseld 3917 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟𝑣𝐵))
136131, 135syl5 34 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣𝐵))
137136pm4.71rd 566 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138137anbi2d 631 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139130, 138bitrd 282 . . . . . . . . 9 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140123, 139syl 17 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141104, 121, 1403bitr4d 314 . . . . . . 7 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
14298, 141syl5rbb 287 . . . . . 6 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
143142eqrelrdv2 5636 . . . . 5 (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14485, 87, 90, 143syl21anc 836 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14579, 144impbida 800 . . 3 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
1461, 12, 28, 145f1ocnv2d 7382 . 2 (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
147 rfovcnvf1od.f . . . 4 𝐹 = (𝐴𝑂𝐵)
148 rfovd.rf . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥𝑎 ↦ {𝑦𝑏𝑥𝑟𝑦})))
149148, 9, 2rfovd 40699 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
150147, 149syl5eq 2848 . . 3 (𝜑𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
151 f1oeq1 6583 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴)))
152 cnveq 5712 . . . . 5 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
153152eqeq1d 2803 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
154151, 153anbi12d 633 . . 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 260 1 (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ 𝐹 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ⊤wtru 1539   ∈ wcel 2112  ∀wral 3109  {crab 3113  Vcvv 3444   ∩ cin 3883   ⊆ wss 3884  𝒫 cpw 4500  ⟨cop 4534   class class class wbr 5033  {copab 5095   ↦ cmpt 5113   × cxp 5521  ◡ccnv 5522  dom cdm 5523  ran crn 5524  Rel wrel 5528   Fn wfn 6323  ⟶wf 6324  –1-1-onto→wf1o 6327  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141   ↑m cmap 8393 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-map 8395 This theorem is referenced by:  rfovcnvd  40703  rfovf1od  40704
 Copyright terms: Public domain W3C validator