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

Theorem fsovrfovd 40703
 Description: The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021.)
Hypotheses
Ref Expression
fsovd.fs 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
fsovd.a (𝜑𝐴𝑉)
fsovd.b (𝜑𝐵𝑊)
fsovd.rf 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢𝑎 ↦ {𝑣𝑏𝑢𝑟𝑣})))
fsovd.cnv 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ 𝑠))
Assertion
Ref Expression
fsovrfovd (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ (𝐴𝑅𝐵))))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑟,𝑢,𝑣   𝐴,𝑠,𝑎,𝑏,𝑓,𝑢,𝑣   𝑥,𝐴,𝑦,𝑎,𝑏,𝑓   𝐵,𝑎,𝑏,𝑓,𝑟,𝑢,𝑣   𝐵,𝑠   𝑦,𝐵   𝑊,𝑎,𝑢   𝜑,𝑎,𝑏,𝑓,𝑟,𝑢,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑠)   𝐵(𝑥)   𝐶(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑅(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑂(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑊(𝑥,𝑦,𝑣,𝑓,𝑠,𝑟,𝑏)

Proof of Theorem fsovrfovd
Dummy variables 𝑐 𝑑 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsovd.b . . . . . 6 (𝜑𝐵𝑊)
2 fsovd.a . . . . . 6 (𝜑𝐴𝑉)
31, 2xpexd 7458 . . . . 5 (𝜑 → (𝐵 × 𝐴) ∈ V)
43adantr 484 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝐵 × 𝐴) ∈ V)
5 elmapi 8415 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
65ffvelrnda 6832 . . . . . . . . . . . . . 14 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
76elpwid 4511 . . . . . . . . . . . . 13 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
87sseld 3917 . . . . . . . . . . . 12 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑢𝐴) → (𝑣 ∈ (𝑓𝑢) → 𝑣𝐵))
98impancom 455 . . . . . . . . . . 11 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑣 ∈ (𝑓𝑢)) → (𝑢𝐴𝑣𝐵))
109pm4.71d 565 . . . . . . . . . 10 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑣 ∈ (𝑓𝑢)) → (𝑢𝐴 ↔ (𝑢𝐴𝑣𝐵)))
1110ex 416 . . . . . . . . 9 (𝑓 ∈ (𝒫 𝐵m 𝐴) → (𝑣 ∈ (𝑓𝑢) → (𝑢𝐴 ↔ (𝑢𝐴𝑣𝐵))))
1211pm5.32rd 581 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐵m 𝐴) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ((𝑢𝐴𝑣𝐵) ∧ 𝑣 ∈ (𝑓𝑢))))
13 ancom 464 . . . . . . . . 9 ((𝑢𝐴𝑣𝐵) ↔ (𝑣𝐵𝑢𝐴))
1413anbi1i 626 . . . . . . . 8 (((𝑢𝐴𝑣𝐵) ∧ 𝑣 ∈ (𝑓𝑢)) ↔ ((𝑣𝐵𝑢𝐴) ∧ 𝑣 ∈ (𝑓𝑢)))
1512, 14syl6bb 290 . . . . . . 7 (𝑓 ∈ (𝒫 𝐵m 𝐴) → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ ((𝑣𝐵𝑢𝐴) ∧ 𝑣 ∈ (𝑓𝑢))))
1615opabbidv 5099 . . . . . 6 (𝑓 ∈ (𝒫 𝐵m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} = {⟨𝑣, 𝑢⟩ ∣ ((𝑣𝐵𝑢𝐴) ∧ 𝑣 ∈ (𝑓𝑢))})
17 opabssxp 5611 . . . . . 6 {⟨𝑣, 𝑢⟩ ∣ ((𝑣𝐵𝑢𝐴) ∧ 𝑣 ∈ (𝑓𝑢))} ⊆ (𝐵 × 𝐴)
1816, 17eqsstrdi 3972 . . . . 5 (𝑓 ∈ (𝒫 𝐵m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ⊆ (𝐵 × 𝐴))
1918adantl 485 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ⊆ (𝐵 × 𝐴))
204, 19sselpwd 5197 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ∈ 𝒫 (𝐵 × 𝐴))
21 eqidd 2802 . . 3 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}))
22 fsovd.rf . . . . 5 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢𝑎 ↦ {𝑣𝑏𝑢𝑟𝑣})))
2322, 1, 2rfovd 40695 . . . 4 (𝜑 → (𝐵𝑅𝐴) = (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢𝐵 ↦ {𝑣𝐴𝑢𝑟𝑣})))
24 breq 5035 . . . . . . . 8 (𝑟 = 𝑡 → (𝑢𝑟𝑣𝑢𝑡𝑣))
2524rabbidv 3430 . . . . . . 7 (𝑟 = 𝑡 → {𝑣𝐴𝑢𝑟𝑣} = {𝑣𝐴𝑢𝑡𝑣})
2625mpteq2dv 5129 . . . . . 6 (𝑟 = 𝑡 → (𝑢𝐵 ↦ {𝑣𝐴𝑢𝑟𝑣}) = (𝑢𝐵 ↦ {𝑣𝐴𝑢𝑡𝑣}))
27 breq1 5036 . . . . . . . . 9 (𝑢 = 𝑐 → (𝑢𝑡𝑣𝑐𝑡𝑣))
2827rabbidv 3430 . . . . . . . 8 (𝑢 = 𝑐 → {𝑣𝐴𝑢𝑡𝑣} = {𝑣𝐴𝑐𝑡𝑣})
29 breq2 5037 . . . . . . . . 9 (𝑣 = 𝑑 → (𝑐𝑡𝑣𝑐𝑡𝑑))
3029cbvrabv 3442 . . . . . . . 8 {𝑣𝐴𝑐𝑡𝑣} = {𝑑𝐴𝑐𝑡𝑑}
3128, 30eqtrdi 2852 . . . . . . 7 (𝑢 = 𝑐 → {𝑣𝐴𝑢𝑡𝑣} = {𝑑𝐴𝑐𝑡𝑑})
3231cbvmptv 5136 . . . . . 6 (𝑢𝐵 ↦ {𝑣𝐴𝑢𝑡𝑣}) = (𝑐𝐵 ↦ {𝑑𝐴𝑐𝑡𝑑})
3326, 32eqtrdi 2852 . . . . 5 (𝑟 = 𝑡 → (𝑢𝐵 ↦ {𝑣𝐴𝑢𝑟𝑣}) = (𝑐𝐵 ↦ {𝑑𝐴𝑐𝑡𝑑}))
3433cbvmptv 5136 . . . 4 (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢𝐵 ↦ {𝑣𝐴𝑢𝑟𝑣})) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐𝐵 ↦ {𝑑𝐴𝑐𝑡𝑑}))
3523, 34eqtrdi 2852 . . 3 (𝜑 → (𝐵𝑅𝐴) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐𝐵 ↦ {𝑑𝐴𝑐𝑡𝑑})))
36 breq 5035 . . . . . . 7 (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → (𝑐𝑡𝑑𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}𝑑))
37 df-br 5034 . . . . . . . 8 (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}𝑑 ↔ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))})
38 vex 3447 . . . . . . . . 9 𝑐 ∈ V
39 vex 3447 . . . . . . . . 9 𝑑 ∈ V
40 eleq1w 2875 . . . . . . . . . 10 (𝑣 = 𝑐 → (𝑣 ∈ (𝑓𝑢) ↔ 𝑐 ∈ (𝑓𝑢)))
4140anbi2d 631 . . . . . . . . 9 (𝑣 = 𝑐 → ((𝑢𝐴𝑣 ∈ (𝑓𝑢)) ↔ (𝑢𝐴𝑐 ∈ (𝑓𝑢))))
42 eleq1w 2875 . . . . . . . . . 10 (𝑢 = 𝑑 → (𝑢𝐴𝑑𝐴))
43 fveq2 6649 . . . . . . . . . . 11 (𝑢 = 𝑑 → (𝑓𝑢) = (𝑓𝑑))
4443eleq2d 2878 . . . . . . . . . 10 (𝑢 = 𝑑 → (𝑐 ∈ (𝑓𝑢) ↔ 𝑐 ∈ (𝑓𝑑)))
4542, 44anbi12d 633 . . . . . . . . 9 (𝑢 = 𝑑 → ((𝑢𝐴𝑐 ∈ (𝑓𝑢)) ↔ (𝑑𝐴𝑐 ∈ (𝑓𝑑))))
4638, 39, 41, 45opelopab 5397 . . . . . . . 8 (⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ↔ (𝑑𝐴𝑐 ∈ (𝑓𝑑)))
4737, 46bitri 278 . . . . . . 7 (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}𝑑 ↔ (𝑑𝐴𝑐 ∈ (𝑓𝑑)))
4836, 47syl6bb 290 . . . . . 6 (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → (𝑐𝑡𝑑 ↔ (𝑑𝐴𝑐 ∈ (𝑓𝑑))))
4948rabbidv 3430 . . . . 5 (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → {𝑑𝐴𝑐𝑡𝑑} = {𝑑𝐴 ∣ (𝑑𝐴𝑐 ∈ (𝑓𝑑))})
5049mpteq2dv 5129 . . . 4 (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → (𝑐𝐵 ↦ {𝑑𝐴𝑐𝑡𝑑}) = (𝑐𝐵 ↦ {𝑑𝐴 ∣ (𝑑𝐴𝑐 ∈ (𝑓𝑑))}))
51 ibar 532 . . . . . . . . 9 (𝑑𝐴 → (𝑐 ∈ (𝑓𝑑) ↔ (𝑑𝐴𝑐 ∈ (𝑓𝑑))))
5251bicomd 226 . . . . . . . 8 (𝑑𝐴 → ((𝑑𝐴𝑐 ∈ (𝑓𝑑)) ↔ 𝑐 ∈ (𝑓𝑑)))
5352rabbiia 3422 . . . . . . 7 {𝑑𝐴 ∣ (𝑑𝐴𝑐 ∈ (𝑓𝑑))} = {𝑑𝐴𝑐 ∈ (𝑓𝑑)}
54 fveq2 6649 . . . . . . . . 9 (𝑑 = 𝑥 → (𝑓𝑑) = (𝑓𝑥))
5554eleq2d 2878 . . . . . . . 8 (𝑑 = 𝑥 → (𝑐 ∈ (𝑓𝑑) ↔ 𝑐 ∈ (𝑓𝑥)))
5655cbvrabv 3442 . . . . . . 7 {𝑑𝐴𝑐 ∈ (𝑓𝑑)} = {𝑥𝐴𝑐 ∈ (𝑓𝑥)}
5753, 56eqtri 2824 . . . . . 6 {𝑑𝐴 ∣ (𝑑𝐴𝑐 ∈ (𝑓𝑑))} = {𝑥𝐴𝑐 ∈ (𝑓𝑥)}
5857mpteq2i 5125 . . . . 5 (𝑐𝐵 ↦ {𝑑𝐴 ∣ (𝑑𝐴𝑐 ∈ (𝑓𝑑))}) = (𝑐𝐵 ↦ {𝑥𝐴𝑐 ∈ (𝑓𝑥)})
59 eleq1w 2875 . . . . . . 7 (𝑐 = 𝑦 → (𝑐 ∈ (𝑓𝑥) ↔ 𝑦 ∈ (𝑓𝑥)))
6059rabbidv 3430 . . . . . 6 (𝑐 = 𝑦 → {𝑥𝐴𝑐 ∈ (𝑓𝑥)} = {𝑥𝐴𝑦 ∈ (𝑓𝑥)})
6160cbvmptv 5136 . . . . 5 (𝑐𝐵 ↦ {𝑥𝐴𝑐 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})
6258, 61eqtri 2824 . . . 4 (𝑐𝐵 ↦ {𝑑𝐴 ∣ (𝑑𝐴𝑐 ∈ (𝑓𝑑))}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})
6350, 62eqtrdi 2852 . . 3 (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → (𝑐𝐵 ↦ {𝑑𝐴𝑐𝑡𝑑}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}))
6420, 21, 35, 63fmptco 6872 . 2 (𝜑 → ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
652, 1xpexd 7458 . . . . . 6 (𝜑 → (𝐴 × 𝐵) ∈ V)
6665adantr 484 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝐴 × 𝐵) ∈ V)
6712opabbidv 5099 . . . . . . 7 (𝑓 ∈ (𝒫 𝐵m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐵) ∧ 𝑣 ∈ (𝑓𝑢))})
68 opabssxp 5611 . . . . . . 7 {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐵) ∧ 𝑣 ∈ (𝑓𝑢))} ⊆ (𝐴 × 𝐵)
6967, 68eqsstrdi 3972 . . . . . 6 (𝑓 ∈ (𝒫 𝐵m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ⊆ (𝐴 × 𝐵))
7069adantl 485 . . . . 5 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ⊆ (𝐴 × 𝐵))
7166, 70sselpwd 5197 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} ∈ 𝒫 (𝐴 × 𝐵))
72 eqid 2801 . . . . 5 (𝐴𝑅𝐵) = (𝐴𝑅𝐵)
7322, 2, 1, 72rfovcnvd 40699 . . . 4 (𝜑(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}))
74 fsovd.cnv . . . . . 6 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ 𝑠))
7574a1i 11 . . . . 5 (𝜑𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ 𝑠)))
76 xpeq12 5548 . . . . . . . 8 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑎 × 𝑏) = (𝐴 × 𝐵))
7776pweqd 4519 . . . . . . 7 ((𝑎 = 𝐴𝑏 = 𝐵) → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝐵))
7877mpteq1d 5122 . . . . . 6 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ 𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ 𝑠))
7978adantl 485 . . . . 5 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵)) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ 𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ 𝑠))
802elexd 3464 . . . . 5 (𝜑𝐴 ∈ V)
811elexd 3464 . . . . 5 (𝜑𝐵 ∈ V)
82 pwexg 5247 . . . . . 6 ((𝐴 × 𝐵) ∈ V → 𝒫 (𝐴 × 𝐵) ∈ V)
83 mptexg 6965 . . . . . 6 (𝒫 (𝐴 × 𝐵) ∈ V → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ 𝑠) ∈ V)
8465, 82, 833syl 18 . . . . 5 (𝜑 → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ 𝑠) ∈ V)
8575, 79, 80, 81, 84ovmpod 7285 . . . 4 (𝜑 → (𝐴𝐶𝐵) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ 𝑠))
86 cnveq 5712 . . . . 5 (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → 𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))})
87 cnvopab 5968 . . . . 5 {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}
8886, 87eqtrdi 2852 . . . 4 (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))} → 𝑠 = {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))})
8971, 73, 85, 88fmptco 6872 . . 3 (𝜑 → ((𝐴𝐶𝐵) ∘ (𝐴𝑅𝐵)) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))}))
9089coeq2d 5701 . 2 (𝜑 → ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ (𝐴𝑅𝐵))) = ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢𝐴𝑣 ∈ (𝑓𝑢))})))
91 fsovd.fs . . 3 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
9291, 2, 1fsovd 40702 . 2 (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
9364, 90, 923eqtr4rd 2847 1 (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ (𝐴𝑅𝐵))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112  {crab 3113  Vcvv 3444   ⊆ wss 3884  𝒫 cpw 4500  ⟨cop 4534   class class class wbr 5033  {copab 5095   ↦ cmpt 5113   × cxp 5521  ◡ccnv 5522   ∘ ccom 5527  ‘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: (None)
 Copyright terms: Public domain W3C validator