Step | Hyp | Ref
| Expression |
1 | | fsovd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
2 | | fsovd.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | 1, 2 | xpexd 7591 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝐴) ∈ V) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐵 × 𝐴) ∈ V) |
5 | | elmapi 8624 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
6 | 5 | ffvelrnda 6953 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵) |
7 | 6 | elpwid 4544 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵) |
8 | 7 | sseld 3919 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → 𝑣 ∈ 𝐵)) |
9 | 8 | impancom 452 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 → 𝑣 ∈ 𝐵)) |
10 | 9 | pm4.71d 562 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵))) |
11 | 10 | ex 413 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)))) |
12 | 11 | pm5.32rd 578 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)))) |
13 | | ancom 461 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ↔ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) |
14 | 13 | anbi1i 624 |
. . . . . . . 8
⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))) |
15 | 12, 14 | bitrdi 287 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)))) |
16 | 15 | opabbidv 5139 |
. . . . . 6
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {〈𝑣, 𝑢〉 ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
17 | | opabssxp 5673 |
. . . . . 6
⊢
{〈𝑣, 𝑢〉 ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴) |
18 | 16, 17 | eqsstrdi 3974 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)) |
19 | 18 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)) |
20 | 4, 19 | sselpwd 5248 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐵 × 𝐴)) |
21 | | eqidd 2739 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
22 | | fsovd.rf |
. . . . 5
⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣}))) |
23 | 22, 1, 2 | rfovd 41590 |
. . . 4
⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}))) |
24 | | breq 5075 |
. . . . . . . 8
⊢ (𝑟 = 𝑡 → (𝑢𝑟𝑣 ↔ 𝑢𝑡𝑣)) |
25 | 24 | rabbidv 3411 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) |
26 | 25 | mpteq2dv 5175 |
. . . . . 6
⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣})) |
27 | | breq1 5076 |
. . . . . . . . 9
⊢ (𝑢 = 𝑐 → (𝑢𝑡𝑣 ↔ 𝑐𝑡𝑣)) |
28 | 27 | rabbidv 3411 |
. . . . . . . 8
⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣}) |
29 | | breq2 5077 |
. . . . . . . . 9
⊢ (𝑣 = 𝑑 → (𝑐𝑡𝑣 ↔ 𝑐𝑡𝑑)) |
30 | 29 | cbvrabv 3423 |
. . . . . . . 8
⊢ {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} |
31 | 28, 30 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) |
32 | 31 | cbvmptv 5186 |
. . . . . 6
⊢ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) |
33 | 26, 32 | eqtrdi 2794 |
. . . . 5
⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})) |
34 | 33 | cbvmptv 5186 |
. . . 4
⊢ (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})) |
35 | 23, 34 | eqtrdi 2794 |
. . 3
⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))) |
36 | | breq 5075 |
. . . . . . 7
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ 𝑐{〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑)) |
37 | | df-br 5074 |
. . . . . . . 8
⊢ (𝑐{〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ 〈𝑐, 𝑑〉 ∈ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
38 | | vex 3433 |
. . . . . . . . 9
⊢ 𝑐 ∈ V |
39 | | vex 3433 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
40 | | eleq1w 2821 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑐 → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑢))) |
41 | 40 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑣 = 𝑐 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)))) |
42 | | eleq1w 2821 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑑 → (𝑢 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴)) |
43 | | fveq2 6766 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑑 → (𝑓‘𝑢) = (𝑓‘𝑑)) |
44 | 43 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑑 → (𝑐 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑑))) |
45 | 42, 44 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑢 = 𝑑 → ((𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))) |
46 | 38, 39, 41, 45 | opelopab 5452 |
. . . . . . . 8
⊢
(〈𝑐, 𝑑〉 ∈ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))) |
47 | 37, 46 | bitri 274 |
. . . . . . 7
⊢ (𝑐{〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))) |
48 | 36, 47 | bitrdi 287 |
. . . . . 6
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))) |
49 | 48 | rabbidv 3411 |
. . . . 5
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) |
50 | 49 | mpteq2dv 5175 |
. . . 4
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))})) |
51 | | ibar 529 |
. . . . . . . . 9
⊢ (𝑑 ∈ 𝐴 → (𝑐 ∈ (𝑓‘𝑑) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))) |
52 | 51 | bicomd 222 |
. . . . . . . 8
⊢ (𝑑 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)) ↔ 𝑐 ∈ (𝑓‘𝑑))) |
53 | 52 | rabbiia 3404 |
. . . . . . 7
⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} |
54 | | fveq2 6766 |
. . . . . . . . 9
⊢ (𝑑 = 𝑥 → (𝑓‘𝑑) = (𝑓‘𝑥)) |
55 | 54 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝑑 = 𝑥 → (𝑐 ∈ (𝑓‘𝑑) ↔ 𝑐 ∈ (𝑓‘𝑥))) |
56 | 55 | cbvrabv 3423 |
. . . . . . 7
⊢ {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} |
57 | 53, 56 | eqtri 2766 |
. . . . . 6
⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} |
58 | 57 | mpteq2i 5178 |
. . . . 5
⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) |
59 | | eleq1w 2821 |
. . . . . . 7
⊢ (𝑐 = 𝑦 → (𝑐 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑓‘𝑥))) |
60 | 59 | rabbidv 3411 |
. . . . . 6
⊢ (𝑐 = 𝑦 → {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
61 | 60 | cbvmptv 5186 |
. . . . 5
⊢ (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
62 | 58, 61 | eqtri 2766 |
. . . 4
⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
63 | 50, 62 | eqtrdi 2794 |
. . 3
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
64 | 20, 21, 35, 63 | fmptco 6993 |
. 2
⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
65 | 2, 1 | xpexd 7591 |
. . . . . 6
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
66 | 65 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V) |
67 | 12 | opabbidv 5139 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
68 | | opabssxp 5673 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵) |
69 | 67, 68 | eqsstrdi 3974 |
. . . . . 6
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)) |
70 | 69 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)) |
71 | 66, 70 | sselpwd 5248 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐴 × 𝐵)) |
72 | | eqid 2738 |
. . . . 5
⊢ (𝐴𝑅𝐵) = (𝐴𝑅𝐵) |
73 | 22, 2, 1, 72 | rfovcnvd 41594 |
. . . 4
⊢ (𝜑 → ◡(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
74 | | fsovd.cnv |
. . . . . 6
⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠)) |
75 | 74 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠))) |
76 | | xpeq12 5609 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 × 𝑏) = (𝐴 × 𝐵)) |
77 | 76 | pweqd 4552 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝐵)) |
78 | 77 | mpteq1d 5168 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠)) |
79 | 78 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠)) |
80 | 2 | elexd 3449 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
81 | 1 | elexd 3449 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
82 | | pwexg 5299 |
. . . . . 6
⊢ ((𝐴 × 𝐵) ∈ V → 𝒫 (𝐴 × 𝐵) ∈ V) |
83 | | mptexg 7089 |
. . . . . 6
⊢
(𝒫 (𝐴
× 𝐵) ∈ V →
(𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V) |
84 | 65, 82, 83 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V) |
85 | 75, 79, 80, 81, 84 | ovmpod 7415 |
. . . 4
⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠)) |
86 | | cnveq 5775 |
. . . . 5
⊢ (𝑠 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = ◡{〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
87 | | cnvopab 6035 |
. . . . 5
⊢ ◡{〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} |
88 | 86, 87 | eqtrdi 2794 |
. . . 4
⊢ (𝑠 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
89 | 71, 73, 85, 88 | fmptco 6993 |
. . 3
⊢ (𝜑 → ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
90 | 89 | coeq2d 5764 |
. 2
⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))) = ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))) |
91 | | fsovd.fs |
. . 3
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
92 | 91, 2, 1 | fsovd 41597 |
. 2
⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
93 | 64, 90, 92 | 3eqtr4rd 2789 |
1
⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)))) |