Step | Hyp | Ref
| Expression |
1 | | fsovd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
2 | | fsovd.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | xpexg 6960 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (𝐵 × 𝐴) ∈ V) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝐴) ∈ V) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝐵 × 𝐴) ∈ V) |
6 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
7 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵) |
8 | 7 | elpwid 4170 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵) |
9 | 8 | sseld 3602 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → 𝑣 ∈ 𝐵)) |
10 | 9 | impancom 456 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 → 𝑣 ∈ 𝐵)) |
11 | 10 | pm4.71d 666 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵))) |
12 | 11 | ex 450 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → (𝑣 ∈ (𝑓‘𝑢) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)))) |
13 | 12 | pm5.32rd 672 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)))) |
14 | | ancom 466 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ↔ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) |
15 | 14 | anbi1i 731 |
. . . . . . . 8
⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))) |
16 | 13, 15 | syl6bb 276 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)))) |
17 | 16 | opabbidv 4716 |
. . . . . 6
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {〈𝑣, 𝑢〉 ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
18 | | opabssxp 5193 |
. . . . . 6
⊢
{〈𝑣, 𝑢〉 ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴) |
19 | 17, 18 | syl6eqss 3655 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)) |
20 | 19 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)) |
21 | 5, 20 | sselpwd 4807 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐵 × 𝐴)) |
22 | | eqidd 2623 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
23 | | fsovd.rf |
. . . . 5
⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣}))) |
24 | 23, 1, 2 | rfovd 38295 |
. . . 4
⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}))) |
25 | | breq 4655 |
. . . . . . . 8
⊢ (𝑟 = 𝑡 → (𝑢𝑟𝑣 ↔ 𝑢𝑡𝑣)) |
26 | 25 | rabbidv 3189 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) |
27 | 26 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣})) |
28 | | breq1 4656 |
. . . . . . . . 9
⊢ (𝑢 = 𝑐 → (𝑢𝑡𝑣 ↔ 𝑐𝑡𝑣)) |
29 | 28 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣}) |
30 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑣 = 𝑑 → (𝑐𝑡𝑣 ↔ 𝑐𝑡𝑑)) |
31 | 30 | cbvrabv 3199 |
. . . . . . . 8
⊢ {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} |
32 | 29, 31 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) |
33 | 32 | cbvmptv 4750 |
. . . . . 6
⊢ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) |
34 | 27, 33 | syl6eq 2672 |
. . . . 5
⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})) |
35 | 34 | cbvmptv 4750 |
. . . 4
⊢ (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})) |
36 | 24, 35 | syl6eq 2672 |
. . 3
⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))) |
37 | | breq 4655 |
. . . . . . 7
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ 𝑐{〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑)) |
38 | | df-br 4654 |
. . . . . . . 8
⊢ (𝑐{〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ 〈𝑐, 𝑑〉 ∈ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
39 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑐 ∈ V |
40 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
41 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑐 → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑢))) |
42 | 41 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑣 = 𝑐 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)))) |
43 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑑 → (𝑢 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴)) |
44 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑑 → (𝑓‘𝑢) = (𝑓‘𝑑)) |
45 | 44 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑑 → (𝑐 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑑))) |
46 | 43, 45 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑢 = 𝑑 → ((𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))) |
47 | 39, 40, 42, 46 | opelopab 4997 |
. . . . . . . 8
⊢
(〈𝑐, 𝑑〉 ∈ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))) |
48 | 38, 47 | bitri 264 |
. . . . . . 7
⊢ (𝑐{〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))) |
49 | 37, 48 | syl6bb 276 |
. . . . . 6
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))) |
50 | 49 | rabbidv 3189 |
. . . . 5
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) |
51 | 50 | mpteq2dv 4745 |
. . . 4
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))})) |
52 | | ibar 525 |
. . . . . . . . 9
⊢ (𝑑 ∈ 𝐴 → (𝑐 ∈ (𝑓‘𝑑) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))) |
53 | 52 | bicomd 213 |
. . . . . . . 8
⊢ (𝑑 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)) ↔ 𝑐 ∈ (𝑓‘𝑑))) |
54 | 53 | rabbiia 3185 |
. . . . . . 7
⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} |
55 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑑 = 𝑥 → (𝑓‘𝑑) = (𝑓‘𝑥)) |
56 | 55 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝑑 = 𝑥 → (𝑐 ∈ (𝑓‘𝑑) ↔ 𝑐 ∈ (𝑓‘𝑥))) |
57 | 56 | cbvrabv 3199 |
. . . . . . 7
⊢ {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} |
58 | 54, 57 | eqtri 2644 |
. . . . . 6
⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} |
59 | 58 | mpteq2i 4741 |
. . . . 5
⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) |
60 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑐 = 𝑦 → (𝑐 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑓‘𝑥))) |
61 | 60 | rabbidv 3189 |
. . . . . 6
⊢ (𝑐 = 𝑦 → {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
62 | 61 | cbvmptv 4750 |
. . . . 5
⊢ (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
63 | 59, 62 | eqtri 2644 |
. . . 4
⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
64 | 51, 63 | syl6eq 2672 |
. . 3
⊢ (𝑡 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
65 | 21, 22, 36, 64 | fmptco 6396 |
. 2
⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
66 | | xpexg 6960 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
67 | 2, 1, 66 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
68 | 67 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝐴 × 𝐵) ∈ V) |
69 | 13 | opabbidv 4716 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
70 | | opabssxp 5193 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵) |
71 | 69, 70 | syl6eqss 3655 |
. . . . . 6
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)) |
72 | 71 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)) |
73 | 68, 72 | sselpwd 4807 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐴 × 𝐵)) |
74 | | eqid 2622 |
. . . . . 6
⊢ (𝐴𝑅𝐵) = (𝐴𝑅𝐵) |
75 | 23, 2, 1, 74 | rfovcnvd 38299 |
. . . . 5
⊢ (𝜑 → ◡(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
76 | 75 | idi 2 |
. . . 4
⊢ (𝜑 → ◡(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
77 | | fsovd.cnv |
. . . . . 6
⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠)) |
78 | 77 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠))) |
79 | | xpeq12 5134 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 × 𝑏) = (𝐴 × 𝐵)) |
80 | 79 | pweqd 4163 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝐵)) |
81 | 80 | mpteq1d 4738 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠)) |
82 | 81 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠)) |
83 | 2 | elexd 3214 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
84 | 1 | elexd 3214 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
85 | | pwexg 4850 |
. . . . . 6
⊢ ((𝐴 × 𝐵) ∈ V → 𝒫 (𝐴 × 𝐵) ∈ V) |
86 | | mptexg 6484 |
. . . . . 6
⊢
(𝒫 (𝐴
× 𝐵) ∈ V →
(𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V) |
87 | 67, 85, 86 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V) |
88 | 78, 82, 83, 84, 87 | ovmpt2d 6788 |
. . . 4
⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠)) |
89 | | cnveq 5296 |
. . . . 5
⊢ (𝑠 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = ◡{〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
90 | | cnvopab 5533 |
. . . . 5
⊢ ◡{〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} |
91 | 89, 90 | syl6eq 2672 |
. . . 4
⊢ (𝑠 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) |
92 | 73, 76, 88, 91 | fmptco 6396 |
. . 3
⊢ (𝜑 → ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) |
93 | 92 | coeq2d 5284 |
. 2
⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))) = ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑣, 𝑢〉 ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))) |
94 | | fsovd.fs |
. . 3
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
95 | 94, 2, 1 | fsovd 38302 |
. 2
⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
96 | 65, 93, 95 | 3eqtr4rd 2667 |
1
⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)))) |