Step | Hyp | Ref
| Expression |
1 | | fsovd.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | ssrab2 4018 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴 |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴) |
4 | 1, 3 | sselpwd 5254 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴) |
6 | 5 | fmpttd 6984 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴) |
7 | 1 | pwexd 5306 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
8 | | fsovd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
9 | 7, 8 | elmapd 8604 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴)) |
10 | 6, 9 | mpbird 256 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵)) |
11 | 10 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵)) |
12 | | fsovfvd.g |
. . . 4
⊢ 𝐺 = (𝐴𝑂𝐵) |
13 | | fsovd.fs |
. . . . 5
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
14 | 13, 1, 8 | fsovd 41578 |
. . . 4
⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
15 | 12, 14 | eqtrid 2792 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
16 | | fsovcnvlem.h |
. . . 4
⊢ 𝐻 = (𝐵𝑂𝐴) |
17 | | oveq2 7277 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → (𝒫 𝑏 ↑m 𝑎) = (𝒫 𝑏 ↑m 𝑑)) |
18 | | rabeq 3417 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) |
19 | 18 | mpteq2dv 5181 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
20 | 17, 19 | mpteq12dv 5170 |
. . . . . . 7
⊢ (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
21 | | pweq 4555 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐) |
22 | 21 | oveq1d 7284 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (𝒫 𝑏 ↑m 𝑑) = (𝒫 𝑐 ↑m 𝑑)) |
23 | | mpteq1 5172 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
24 | 22, 23 | mpteq12dv 5170 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
25 | 20, 24 | cbvmpov 7362 |
. . . . . 6
⊢ (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) |
26 | | eqid 2740 |
. . . . . . 7
⊢ V =
V |
27 | | fveq1 6768 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
28 | 27 | eleq2d 2826 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑔‘𝑥))) |
29 | 28 | rabbidv 3413 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) |
30 | 29 | mpteq2dv 5181 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) |
31 | 30 | cbvmptv 5192 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) |
32 | | eleq1w 2823 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑢 → (𝑦 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑥))) |
33 | 32 | rabbidv 3413 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑢 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) |
34 | 33 | cbvmptv 5192 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) |
35 | | fveq2 6769 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → (𝑔‘𝑥) = (𝑔‘𝑣)) |
36 | 35 | eleq2d 2826 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (𝑢 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑣))) |
37 | 36 | cbvrabv 3425 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)} = {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)} |
38 | 37 | mpteq2i 5184 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}) |
39 | 34, 38 | eqtri 2768 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}) |
40 | 39 | mpteq2i 5184 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})) |
41 | 31, 40 | eqtri 2768 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})) |
42 | 26, 26, 41 | mpoeq123i 7343 |
. . . . . 6
⊢ (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
43 | 13, 25, 42 | 3eqtri 2772 |
. . . . 5
⊢ 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
44 | 43, 8, 1 | fsovd 41578 |
. . . 4
⊢ (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
45 | 16, 44 | eqtrid 2792 |
. . 3
⊢ (𝜑 → 𝐻 = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}))) |
46 | | fveq1 6768 |
. . . . . 6
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑔‘𝑣) = ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)) |
47 | 46 | eleq2d 2826 |
. . . . 5
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ (𝑔‘𝑣) ↔ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣))) |
48 | 47 | rabbidv 3413 |
. . . 4
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) |
49 | 48 | mpteq2dv 5181 |
. . 3
⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) |
50 | 11, 15, 45, 49 | fmptco 6996 |
. 2
⊢ (𝜑 → (𝐻 ∘ 𝐺) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}))) |
51 | | eqidd 2741 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})) |
52 | | eleq1w 2823 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑥))) |
53 | 52 | rabbidv 3413 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}) |
54 | 53 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) ∧ 𝑦 = 𝑣) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}) |
55 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵) |
56 | | rabexg 5259 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V) |
57 | 1, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V) |
58 | 57 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V) |
59 | 51, 54, 55, 58 | fvmptd 6877 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}) |
60 | 59 | eleq2d 2826 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})) |
61 | | fveq2 6769 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (𝑓‘𝑥) = (𝑓‘𝑢)) |
62 | 61 | eleq2d 2826 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝑣 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢))) |
63 | 62 | elrab3 3627 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝐴 → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢))) |
64 | 63 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢))) |
65 | 60, 64 | bitrd 278 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓‘𝑢))) |
66 | 65 | rabbidva 3411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}) |
67 | 66 | adantlr 712 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}) |
68 | | elmapi 8612 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
69 | 68 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
70 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) |
71 | 69, 70 | ffvelrnd 6957 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵) |
72 | 71 | elpwid 4550 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵) |
73 | | sseqin2 4155 |
. . . . . . . 8
⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢)) |
74 | 72, 73 | sylib 217 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢)) |
75 | | dfin5 3900 |
. . . . . . 7
⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)} |
76 | 74, 75 | eqtr3di 2795 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}) |
77 | 67, 76 | eqtr4d 2783 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = (𝑓‘𝑢)) |
78 | 77 | mpteq2dva 5179 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢))) |
79 | 68 | feqmptd 6832 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢))) |
80 | 79 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢))) |
81 | 78, 80 | eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = 𝑓) |
82 | 81 | mpteq2dva 5179 |
. 2
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓)) |
83 | | mptresid 5956 |
. . . 4
⊢ ( I
↾ (𝒫 𝐵
↑m 𝐴)) =
(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) |
84 | 83 | eqcomi 2749 |
. . 3
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)) |
85 | 84 | a1i 11 |
. 2
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴))) |
86 | 50, 82, 85 | 3eqtrd 2784 |
1
⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑m 𝐴))) |