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 41565
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 2739 . . 3 (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
2 rfovd.b . . . . . . . 8 (𝜑𝐵𝑊)
3 ssrab2 4017 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵
43a1i 11 . . . . . . . 8 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ⊆ 𝐵)
52, 4sselpwd 5253 . . . . . . 7 (𝜑 → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
65adantr 480 . . . . . 6 ((𝜑𝑥𝐴) → {𝑦𝐵𝑥𝑟𝑦} ∈ 𝒫 𝐵)
76fmpttd 6983 . . . . 5 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)
82pwexd 5305 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
9 rfovd.a . . . . . 6 (𝜑𝐴𝑉)
108, 9elmapd 8603 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴) ↔ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵))
117, 10mpbird 256 . . . 4 (𝜑 → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴))
1211adantr 480 . . 3 ((𝜑𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) ∈ (𝒫 𝐵m 𝐴))
139, 2xpexd 7592 . . . . 5 (𝜑 → (𝐴 × 𝐵) ∈ V)
1413adantr 480 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝐴 × 𝐵) ∈ V)
158, 9elmapd 8603 . . . . . . . . . . . 12 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵))
1615biimpa 476 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵)
1716ffvelrnda 6955 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 𝒫 𝐵)
1817ex 412 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝒫 𝐵))
19 elpwi 4547 . . . . . . . . . 10 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑓𝑥) ⊆ 𝐵)
2019sseld 3924 . . . . . . . . 9 ((𝑓𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵))
2118, 20syl6 35 . . . . . . . 8 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑥𝐴 → (𝑦 ∈ (𝑓𝑥) → 𝑦𝐵)))
2221imdistand 570 . . . . . . 7 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → (𝑥𝐴𝑦𝐵)))
23 trud 1551 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ⊤)
2422, 23jca2 513 . . . . . 6 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) → ((𝑥𝐴𝑦𝐵) ∧ ⊤)))
2524ssopab2dv 5465 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)})
26 opabssxp 5677 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵)
2725, 26sstrdi 3937 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ⊆ (𝐴 × 𝐵))
2814, 27sselpwd 5253 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ∈ 𝒫 (𝐴 × 𝐵))
29 simplrr 774 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 ∈ (𝒫 𝐵m 𝐴))
30 elmapfn 8627 . . . . . 6 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓 Fn 𝐴)
3129, 30syl 17 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 Fn 𝐴)
322ad2antrr 722 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝐵𝑊)
33 rabexg 5258 . . . . . . 7 (𝐵𝑊 → {𝑦𝐵𝑥𝑟𝑦} ∈ V)
3433ralrimivw 3110 . . . . . 6 (𝐵𝑊 → ∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V)
35 nfcv 2908 . . . . . . 7 𝑥𝐴
3635fnmptf 6565 . . . . . 6 (∀𝑥𝐴 {𝑦𝐵𝑥𝑟𝑦} ∈ V → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
3732, 34, 363syl 18 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) Fn 𝐴)
38 dfin5 3899 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑏𝐵𝑏 ∈ (𝑓𝑢)}
39 simpllr 772 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴)))
40 elmapi 8611 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
4139, 40simpl2im 503 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
42 simpr 484 . . . . . . . . . 10 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝑢𝐴)
4341, 42ffvelrnd 6956 . . . . . . . . 9 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
4443elpwid 4549 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
45 sseqin2 4154 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
4644, 45sylib 217 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
47 ibar 528 . . . . . . . . 9 (𝑢𝐴 → (𝑏 ∈ (𝑓𝑢) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
4847rabbidv 3412 . . . . . . . 8 (𝑢𝐴 → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
4948adantl 481 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵𝑏 ∈ (𝑓𝑢)} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
5038, 46, 493eqtr3a 2803 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
51 breq2 5082 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑥𝑟𝑦𝑥𝑟𝑏))
5251cbvrabv 3424 . . . . . . . . 9 {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑥𝑟𝑏}
53 breq1 5081 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝑟𝑏𝑎𝑟𝑏))
54 df-br 5079 . . . . . . . . . . 11 (𝑎𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟)
5553, 54bitrdi 286 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑟))
5655rabbidv 3412 . . . . . . . . 9 (𝑥 = 𝑎 → {𝑏𝐵𝑥𝑟𝑏} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5752, 56eqtrid 2791 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
5857cbvmptv 5191 . . . . . . 7 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟})
59 simpr 484 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢)
6059opeq1d 4815 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑏⟩)
61 simpllr 772 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
6260, 61eleq12d 2834 . . . . . . . . 9 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
63 vex 3434 . . . . . . . . . 10 𝑢 ∈ V
64 vex 3434 . . . . . . . . . 10 𝑏 ∈ V
65 simpl 482 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑥 = 𝑢)
6665eleq1d 2824 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑥𝐴𝑢𝐴))
67 simpr 484 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → 𝑦 = 𝑏)
6865fveq2d 6772 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑓𝑥) = (𝑓𝑢))
6967, 68eleq12d 2834 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑏) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑏 ∈ (𝑓𝑢)))
7066, 69anbi12d 630 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑏) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7163, 64, 70opelopaba 5450 . . . . . . . . 9 (⟨𝑢, 𝑏⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢)))
7262, 71bitrdi 286 . . . . . . . 8 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → (⟨𝑎, 𝑏⟩ ∈ 𝑟 ↔ (𝑢𝐴𝑏 ∈ (𝑓𝑢))))
7372rabbidv 3412 . . . . . . 7 (((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵 ∣ ⟨𝑎, 𝑏⟩ ∈ 𝑟} = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
742ad3antrrr 726 . . . . . . . 8 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → 𝐵𝑊)
75 rabexg 5258 . . . . . . . 8 (𝐵𝑊 → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7674, 75syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))} ∈ V)
7758, 73, 42, 76fvmptd2 6877 . . . . . 6 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢) = {𝑏𝐵 ∣ (𝑢𝐴𝑏 ∈ (𝑓𝑢))})
7850, 77eqtr4d 2782 . . . . 5 ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ 𝑢𝐴) → (𝑓𝑢) = ((𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})‘𝑢))
7931, 37, 78eqfnfvd 6906 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
80 simplrl 773 . . . . . . . 8 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
8180elpwid 4549 . . . . . . 7 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
82 xpss 5604 . . . . . . 7 (𝐴 × 𝐵) ⊆ (V × V)
8381, 82sstrdi 3937 . . . . . 6 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V))
84 df-rel 5595 . . . . . 6 (Rel 𝑟𝑟 ⊆ (V × V))
8583, 84sylibr 233 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel 𝑟)
86 relopabv 5728 . . . . . 6 Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}
8786a1i 11 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
88 simpl 482 . . . . . . 7 ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
892, 88anim12i 612 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) → (𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)))
9089anim1i 614 . . . . 5 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
91 vex 3434 . . . . . . . 8 𝑣 ∈ V
92 simpl 482 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
9392eleq1d 2824 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝐴𝑢𝐴))
94 simpr 484 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
9592fveq2d 6772 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑓𝑥) = (𝑓𝑢))
9694, 95eleq12d 2834 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
9793, 96anbi12d 630 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝐴𝑦 ∈ (𝑓𝑥)) ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢))))
9863, 91, 97opelopaba 5450 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ (𝑢𝐴𝑣 ∈ (𝑓𝑢)))
99 breq2 5082 . . . . . . . . . . . 12 (𝑏 = 𝑣 → (𝑢𝑟𝑏𝑢𝑟𝑣))
100 df-br 5079 . . . . . . . . . . . 12 (𝑢𝑟𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟)
10199, 100bitrdi 286 . . . . . . . . . . 11 (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
102101elrab 3625 . . . . . . . . . 10 (𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏} ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
103102anbi2i 622 . . . . . . . . 9 ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
104103a1i 11 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
105 simplr 765 . . . . . . . . . . . 12 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))
106 breq1 5081 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝑥𝑟𝑦𝑎𝑟𝑦))
107106rabbidv 3412 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑦𝐵𝑎𝑟𝑦})
108 breq2 5082 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (𝑎𝑟𝑦𝑎𝑟𝑏))
109108cbvrabv 3424 . . . . . . . . . . . . . 14 {𝑦𝐵𝑎𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏}
110107, 109eqtrdi 2795 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → {𝑦𝐵𝑥𝑟𝑦} = {𝑏𝐵𝑎𝑟𝑏})
111110cbvmptv 5191 . . . . . . . . . . . 12 (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}) = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏})
112105, 111eqtrdi 2795 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑓 = (𝑎𝐴 ↦ {𝑏𝐵𝑎𝑟𝑏}))
113 breq1 5081 . . . . . . . . . . . . 13 (𝑎 = 𝑢 → (𝑎𝑟𝑏𝑢𝑟𝑏))
114113rabbidv 3412 . . . . . . . . . . . 12 (𝑎 = 𝑢 → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
115114adantl 481 . . . . . . . . . . 11 (((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) ∧ 𝑎 = 𝑢) → {𝑏𝐵𝑎𝑟𝑏} = {𝑏𝐵𝑢𝑟𝑏})
116 simpr 484 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → 𝑢𝐴)
117 rabexg 5258 . . . . . . . . . . . 12 (𝐵𝑊 → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
118117ad3antrrr 726 . . . . . . . . . . 11 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → {𝑏𝐵𝑢𝑟𝑏} ∈ V)
119112, 115, 116, 118fvmptd 6876 . . . . . . . . . 10 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑏𝐵𝑢𝑟𝑏})
120119eleq2d 2825 . . . . . . . . 9 ((((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) ∧ 𝑢𝐴) → (𝑣 ∈ (𝑓𝑢) ↔ 𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏}))
121120pm5.32da 578 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ (𝑢𝐴𝑣 ∈ {𝑏𝐵𝑢𝑟𝑏})))
122 simplr 765 . . . . . . . . . 10 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵))
123122elpwid 4549 . . . . . . . . 9 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵))
12463, 91opeldm 5813 . . . . . . . . . . . 12 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢 ∈ dom 𝑟)
125 dmss 5808 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵))
126 dmxpss 6071 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐵) ⊆ 𝐴
127125, 126sstrdi 3937 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟𝐴)
128127sseld 3924 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟𝑢𝐴))
129124, 128syl5 34 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑢𝐴))
130129pm4.71rd 562 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
13163, 91opelrn 5849 . . . . . . . . . . . . 13 (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣 ∈ ran 𝑟)
132 rnss 5845 . . . . . . . . . . . . . . 15 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵))
133 rnxpss 6072 . . . . . . . . . . . . . . 15 ran (𝐴 × 𝐵) ⊆ 𝐵
134132, 133sstrdi 3937 . . . . . . . . . . . . . 14 (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟𝐵)
135134sseld 3924 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟𝑣𝐵))
136131, 135syl5 34 . . . . . . . . . . . 12 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟𝑣𝐵))
137136pm4.71rd 562 . . . . . . . . . . 11 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟)))
138137anbi2d 628 . . . . . . . . . 10 (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢𝐴 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟) ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
139130, 138bitrd 278 . . . . . . . . 9 (𝑟 ⊆ (𝐴 × 𝐵) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
140123, 139syl 17 . . . . . . . 8 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ (𝑢𝐴 ∧ (𝑣𝐵 ∧ ⟨𝑢, 𝑣⟩ ∈ 𝑟))))
141104, 121, 1403bitr4d 310 . . . . . . 7 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑟))
14298, 141bitr2id 283 . . . . . 6 (((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (⟨𝑢, 𝑣⟩ ∈ 𝑟 ↔ ⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}))
143142eqrelrdv2 5702 . . . . 5 (((Rel 𝑟 ∧ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ∧ ((𝐵𝑊𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦}))) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14485, 87, 90, 143syl21anc 834 . . . 4 (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) ∧ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
14579, 144impbida 797 . . 3 ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴))) → (𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))} ↔ 𝑓 = (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
1461, 12, 28, 145f1ocnv2d 7513 . 2 (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
147 rfovcnvf1od.f . . . 4 𝐹 = (𝐴𝑂𝐵)
148 rfovd.rf . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥𝑎 ↦ {𝑦𝑏𝑥𝑟𝑦})))
149148, 9, 2rfovd 41562 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
150147, 149eqtrid 2791 . . 3 (𝜑𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
151 f1oeq1 6700 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵m 𝐴)))
152 cnveq 5779 . . . . 5 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})))
153152eqeq1d 2741 . . . 4 (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) → (𝐹 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥𝐴 ↦ {𝑦𝐵𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})))
154151, 153anbi12d 630 . . 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 395   = wceq 1541  wtru 1542  wcel 2109  wral 3065  {crab 3069  Vcvv 3430  cin 3890  wss 3891  𝒫 cpw 4538  cop 4572   class class class wbr 5078  {copab 5140  cmpt 5161   × cxp 5586  ccnv 5587  dom cdm 5588  ran crn 5589  Rel wrel 5593   Fn wfn 6425  wf 6426  1-1-ontowf1o 6429  cfv 6430  (class class class)co 7268  cmpo 7270  m cmap 8589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-oprab 7272  df-mpo 7273  df-1st 7817  df-2nd 7818  df-map 8591
This theorem is referenced by:  rfovcnvd  41566  rfovf1od  41567
  Copyright terms: Public domain W3C validator