Metamath Proof Explorer

Theorem fsovcnvlem

Description: The O operator, which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021)

Ref Expression
Hypotheses fsovd.fs ⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
fsovd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fsovd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
fsovfvd.g ⊢ 𝐺 = ( 𝐴 𝑂 𝐵 )
fsovcnvlem.h ⊢ 𝐻 = ( 𝐵 𝑂 𝐴 )
Assertion fsovcnvlem ( 𝜑 → ( 𝐻 ∘ 𝐺 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝐴 ) ) )

Proof

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 elmapi ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
69 68 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
70 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ 𝐴 )
71 69 70 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) ∈ 𝒫 𝐵 )
72 71 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) ⊆ 𝐵 )
73 sseqin2 ⊢ ( ( 𝑓 ‘ 𝑢 ) ⊆ 𝐵 ↔ ( 𝐵 ∩ ( 𝑓 ‘ 𝑢 ) ) = ( 𝑓 ‘ 𝑢 ) )
74 72 73 sylib ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝐵 ∩ ( 𝑓 ‘ 𝑢 ) ) = ( 𝑓 ‘ 𝑢 ) )
75 dfin5 ⊢ ( 𝐵 ∩ ( 𝑓 ‘ 𝑢 ) ) = { 𝑣 ∈ 𝐵 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) }
76 74 75 eqtr3di ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) = { 𝑣 ∈ 𝐵 ∣ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) } )
77 67 76 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } = ( 𝑓 ‘ 𝑢 ) )
78 77 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝑢 ∈ 𝐴 ↦ { 𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ( ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ‘ 𝑣 ) } ) = ( 𝑢 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑢 ) ) )
79 68 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 𝐴 ) ) )