Step | Hyp | Ref
| Expression |
1 | | fsovd.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴 |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴) |
4 | 1, 3 | sselpwd 4734 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴) |
6 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
7 | 5, 6 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴) |
8 | | pwexg 4776 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
9 | 1, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
10 | | fsovd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
11 | 9, 10 | elmapd 7758 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴)) |
12 | 7, 11 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑𝑚 𝐵)) |
13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑𝑚 𝐵)) |
14 | | fsovfvd.g |
. . . 4
⊢ 𝐺 = (𝐴𝑂𝐵) |
15 | | fsovd.fs |
. . . . 5
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
16 | 15, 1, 10 | fsovd 37322 |
. . . 4
⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
17 | 14, 16 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
18 | | fsovcnvlem.h |
. . . 4
⊢ 𝐻 = (𝐵𝑂𝐴) |
19 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → (𝒫 𝑏 ↑𝑚 𝑎) = (𝒫 𝑏 ↑𝑚
𝑑)) |
20 | | rabeq 3166 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
21 | 20 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
22 | 19, 21 | mpteq12dv 4663 |
. . . . . . 7
⊢ (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
23 | | pweq 4111 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐) |
24 | 23 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (𝒫 𝑏 ↑𝑚 𝑑) = (𝒫 𝑐 ↑𝑚
𝑑)) |
25 | | mpteq1 4665 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
26 | 24, 25 | mpteq12dv 4663 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
27 | 22, 26 | cbvmpt2v 6633 |
. . . . . 6
⊢ (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
28 | | eqid 2610 |
. . . . . . 7
⊢ V =
V |
29 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
30 | 29 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑔‘𝑥))) |
31 | 30 | rabbidv 3164 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) |
32 | 31 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) |
33 | 32 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝑐 ↑𝑚
𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) |
34 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑢 → (𝑦 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑥))) |
35 | 34 | rabbidv 3164 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑢 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) |
36 | 35 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) |
37 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → (𝑔‘𝑥) = (𝑔‘𝑣)) |
38 | 37 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (𝑢 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑣))) |
39 | 38 | cbvrabv 3172 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)} = {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)} |
40 | 39 | mpteq2i 4669 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}) |
41 | 36, 40 | eqtri 2632 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}) |
42 | 41 | mpteq2i 4669 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝑐 ↑𝑚
𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})) |
43 | 33, 42 | eqtri 2632 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝑐 ↑𝑚
𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})) |
44 | 28, 28, 43 | mpt2eq123i 6616 |
. . . . . 6
⊢ (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
45 | 15, 27, 44 | 3eqtri 2636 |
. . . . 5
⊢ 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑𝑚 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
46 | 45, 10, 1 | fsovd 37322 |
. . . 4
⊢ (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴 ↑𝑚 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
47 | 18, 46 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝐻 = (𝑔 ∈ (𝒫 𝐴 ↑𝑚 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
48 | | fveq1 6102 |
. . . . . 6
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑔‘𝑣) = ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)) |
49 | 48 | eleq2d 2673 |
. . . . 5
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ (𝑔‘𝑣) ↔ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣))) |
50 | 49 | rabbidv 3164 |
. . . 4
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) |
51 | 50 | mpteq2dv 4673 |
. . 3
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) |
52 | 13, 17, 47, 51 | fmptco 6303 |
. 2
⊢ (𝜑 → (𝐻 ∘ 𝐺) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}))) |
53 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
54 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑥))) |
55 | 54 | rabbidv 3164 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}) |
56 | 55 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) ∧ 𝑦 = 𝑣) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}) |
57 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵) |
58 | | rabexg 4739 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V) |
59 | 1, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V) |
60 | 59 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V) |
61 | 53, 56, 57, 60 | fvmptd 6197 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}) |
62 | 61 | eleq2d 2673 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})) |
63 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (𝑓‘𝑥) = (𝑓‘𝑢)) |
64 | 63 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝑣 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢))) |
65 | 64 | elrab3 3332 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝐴 → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢))) |
66 | 65 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢))) |
67 | 62, 66 | bitrd 267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓‘𝑢))) |
68 | 67 | rabbidva 3163 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}) |
69 | 68 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}) |
70 | | dfin5 3548 |
. . . . . . 7
⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)} |
71 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
72 | 71 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
73 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) |
74 | 72, 73 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵) |
75 | 74 | elpwid 4118 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵) |
76 | | sseqin2 3779 |
. . . . . . . 8
⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢)) |
77 | 75, 76 | sylib 207 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢)) |
78 | 70, 77 | syl5reqr 2659 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}) |
79 | 69, 78 | eqtr4d 2647 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = (𝑓‘𝑢)) |
80 | 79 | mpteq2dva 4672 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢))) |
81 | 71 | feqmptd 6159 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢))) |
82 | 81 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢))) |
83 | 80, 82 | eqtr4d 2647 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = 𝑓) |
84 | 83 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ 𝑓)) |
85 | | mptresid 5375 |
. . 3
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑𝑚
𝐴)) |
86 | 85 | a1i 11 |
. 2
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑𝑚 𝐴))) |
87 | 52, 84, 86 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑𝑚 𝐴))) |