Step |
Hyp |
Ref |
Expression |
1 |
|
fsovd.fs |
⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |
2 |
|
fsovd.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
3 |
|
fsovd.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) |
4 |
|
fsovfvd.g |
⊢ 𝐺 = ( 𝐴 𝑂 𝐵 ) |
5 |
|
fsovcnvlem.h |
⊢ 𝐻 = ( 𝐵 𝑂 𝐴 ) |
6 |
|
ssrab2 |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ⊆ 𝐴 |
7 |
6
|
a1i |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ⊆ 𝐴 ) |
8 |
2 7
|
sselpwd |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ 𝒫 𝐴 ) |
9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ 𝒫 𝐴 ) |
10 |
9
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) : 𝐵 ⟶ 𝒫 𝐴 ) |
11 |
2
|
pwexd |
⊢ ( 𝜑 → 𝒫 𝐴 ∈ V ) |
12 |
11 3
|
elmapd |
⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) : 𝐵 ⟶ 𝒫 𝐴 ) ) |
13 |
10 12
|
mpbird |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ) |
15 |
1 2 3
|
fsovd |
⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |
16 |
4 15
|
syl5eq |
⊢ ( 𝜑 → 𝐺 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |
17 |
|
oveq2 |
⊢ ( 𝑎 = 𝑑 → ( 𝒫 𝑏 ↑m 𝑎 ) = ( 𝒫 𝑏 ↑m 𝑑 ) ) |
18 |
|
rabeq |
⊢ ( 𝑎 = 𝑑 → { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) |
19 |
18
|
mpteq2dv |
⊢ ( 𝑎 = 𝑑 → ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) |
20 |
17 19
|
mpteq12dv |
⊢ ( 𝑎 = 𝑑 → ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) = ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |
21 |
|
pweq |
⊢ ( 𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐 ) |
22 |
21
|
oveq1d |
⊢ ( 𝑏 = 𝑐 → ( 𝒫 𝑏 ↑m 𝑑 ) = ( 𝒫 𝑐 ↑m 𝑑 ) ) |
23 |
|
mpteq1 |
⊢ ( 𝑏 = 𝑐 → ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) |
24 |
22 23
|
mpteq12dv |
⊢ ( 𝑏 = 𝑐 → ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) = ( 𝑓 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |
25 |
20 24
|
cbvmpov |
⊢ ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) = ( 𝑑 ∈ V , 𝑐 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |
26 |
|
eqid |
⊢ V = V |
27 |
|
fveq1 |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) |
28 |
27
|
eleq2d |
⊢ ( 𝑓 = 𝑔 → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ) ) |
29 |
28
|
rabbidv |
⊢ ( 𝑓 = 𝑔 → { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } ) |
30 |
29
|
mpteq2dv |
⊢ ( 𝑓 = 𝑔 → ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } ) ) |
31 |
30
|
cbvmptv |
⊢ ( 𝑓 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) = ( 𝑔 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } ) ) |
32 |
|
eleq1w |
⊢ ( 𝑦 = 𝑢 → ( 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) ↔ 𝑢 ∈ ( 𝑔 ‘ 𝑥 ) ) ) |
33 |
32
|
rabbidv |
⊢ ( 𝑦 = 𝑢 → { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } = { 𝑥 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑥 ) } ) |
34 |
33
|
cbvmptv |
⊢ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } ) = ( 𝑢 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑥 ) } ) |
35 |
|
fveq2 |
⊢ ( 𝑥 = 𝑣 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑣 ) ) |
36 |
35
|
eleq2d |
⊢ ( 𝑥 = 𝑣 → ( 𝑢 ∈ ( 𝑔 ‘ 𝑥 ) ↔ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) ) ) |
37 |
36
|
cbvrabv |
⊢ { 𝑥 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑥 ) } = { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } |
38 |
37
|
mpteq2i |
⊢ ( 𝑢 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑥 ) } ) = ( 𝑢 ∈ 𝑐 ↦ { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) |
39 |
34 38
|
eqtri |
⊢ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } ) = ( 𝑢 ∈ 𝑐 ↦ { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) |
40 |
39
|
mpteq2i |
⊢ ( 𝑔 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑔 ‘ 𝑥 ) } ) ) = ( 𝑔 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑢 ∈ 𝑐 ↦ { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) ) |
41 |
31 40
|
eqtri |
⊢ ( 𝑓 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) = ( 𝑔 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑢 ∈ 𝑐 ↦ { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) ) |
42 |
26 26 41
|
mpoeq123i |
⊢ ( 𝑑 ∈ V , 𝑐 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑦 ∈ 𝑐 ↦ { 𝑥 ∈ 𝑑 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) = ( 𝑑 ∈ V , 𝑐 ∈ V ↦ ( 𝑔 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑢 ∈ 𝑐 ↦ { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) ) ) |
43 |
1 25 42
|
3eqtri |
⊢ 𝑂 = ( 𝑑 ∈ V , 𝑐 ∈ V ↦ ( 𝑔 ∈ ( 𝒫 𝑐 ↑m 𝑑 ) ↦ ( 𝑢 ∈ 𝑐 ↦ { 𝑣 ∈ 𝑑 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) ) ) |
44 |
43 3 2
|
fsovd |
⊢ ( 𝜑 → ( 𝐵 𝑂 𝐴 ) = ( 𝑔 ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ↦ ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) ) ) |
45 |
5 44
|
syl5eq |
⊢ ( 𝜑 → 𝐻 = ( 𝑔 ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ↦ ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) ) ) |
46 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) → ( 𝑔 ‘ 𝑣 ) = ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) ) |
47 |
46
|
eleq2d |
⊢ ( 𝑔 = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) → ( 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) ↔ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) ) ) |
48 |
47
|
rabbidv |
⊢ ( 𝑔 = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) → { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } = { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) |
49 |
48
|
mpteq2dv |
⊢ ( 𝑔 = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) → ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( 𝑔 ‘ 𝑣 ) } ) = ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) ) |
50 |
14 16 45 49
|
fmptco |
⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) ) ) |
51 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) |
52 |
|
eleq1w |
⊢ ( 𝑦 = 𝑣 → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) ) ) |
53 |
52
|
rabbidv |
⊢ ( 𝑦 = 𝑣 → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ) |
54 |
53
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑦 = 𝑣 ) → { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ) |
55 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 ) |
56 |
|
rabexg |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ V ) |
57 |
2 56
|
syl |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ V ) |
58 |
57
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ V ) |
59 |
51 54 55 58
|
fvmptd |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) = { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ) |
60 |
59
|
eleq2d |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) ↔ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) |
61 |
|
fveq2 |
⊢ ( 𝑥 = 𝑢 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑢 ) ) |
62 |
61
|
eleq2d |
⊢ ( 𝑥 = 𝑢 → ( 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) ↔ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
63 |
62
|
elrab3 |
⊢ ( 𝑢 ∈ 𝐴 → ( 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ↔ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
64 |
63
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑥 ) } ↔ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
65 |
60 64
|
bitrd |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) ↔ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
66 |
65
|
rabbidva |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } = { 𝑣 ∈ 𝐵 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) } ) |
67 |
66
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } = { 𝑣 ∈ 𝐵 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) } ) |
68 |
|
dfin5 |
⊢ ( 𝐵 ∩ ( 𝑓 ‘ 𝑢 ) ) = { 𝑣 ∈ 𝐵 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) } |
69 |
|
elmapi |
⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 ) |
70 |
69
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 ) |
71 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ 𝐴 ) |
72 |
70 71
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) ∈ 𝒫 𝐵 ) |
73 |
72
|
elpwid |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) ⊆ 𝐵 ) |
74 |
|
sseqin2 |
⊢ ( ( 𝑓 ‘ 𝑢 ) ⊆ 𝐵 ↔ ( 𝐵 ∩ ( 𝑓 ‘ 𝑢 ) ) = ( 𝑓 ‘ 𝑢 ) ) |
75 |
73 74
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝐵 ∩ ( 𝑓 ‘ 𝑢 ) ) = ( 𝑓 ‘ 𝑢 ) ) |
76 |
68 75
|
syl5reqr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) = { 𝑣 ∈ 𝐵 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) } ) |
77 |
67 76
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } = ( 𝑓 ‘ 𝑢 ) ) |
78 |
77
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) = ( 𝑢 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑢 ) ) ) |
79 |
69
|
feqmptd |
⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝑓 = ( 𝑢 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑢 ) ) ) |
80 |
79
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → 𝑓 = ( 𝑢 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑢 ) ) ) |
81 |
78 80
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) = 𝑓 ) |
82 |
81
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ 𝑓 ) ) |
83 |
|
mptresid |
⊢ ( I ↾ ( 𝒫 𝐵 ↑m 𝐴 ) ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ 𝑓 ) |
84 |
83
|
eqcomi |
⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ 𝑓 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝐴 ) ) |
85 |
84
|
a1i |
⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ 𝑓 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝐴 ) ) ) |
86 |
50 82 85
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝐴 ) ) ) |