Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fsovcnvlem Structured version   Visualization version   GIF version

Theorem fsovcnvlem 37327
 Description: The 𝑂 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.)
Hypotheses
Ref Expression
fsovd.fs 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
fsovd.a (𝜑𝐴𝑉)
fsovd.b (𝜑𝐵𝑊)
fsovfvd.g 𝐺 = (𝐴𝑂𝐵)
fsovcnvlem.h 𝐻 = (𝐵𝑂𝐴)
Assertion
Ref Expression
fsovcnvlem (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑥,𝑦   𝐵,𝑎,𝑏,𝑓,𝑦   𝜑,𝑎,𝑏,𝑓,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐺(𝑥,𝑦,𝑓,𝑎,𝑏)   𝐻(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑂(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑊(𝑥,𝑦,𝑓,𝑎,𝑏)

Proof of Theorem fsovcnvlem
Dummy variables 𝑐 𝑑 𝑔 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsovd.a . . . . . . . 8 (𝜑𝐴𝑉)
2 ssrab2 3650 . . . . . . . . 9 {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴
32a1i 11 . . . . . . . 8 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴)
41, 3sselpwd 4734 . . . . . . 7 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
54adantr 480 . . . . . 6 ((𝜑𝑦𝐵) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
6 eqid 2610 . . . . . 6 (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})
75, 6fmptd 6292 . . . . 5 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴)
8 pwexg 4776 . . . . . . 7 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
91, 8syl 17 . . . . . 6 (𝜑 → 𝒫 𝐴 ∈ V)
10 fsovd.b . . . . . 6 (𝜑𝐵𝑊)
119, 10elmapd 7758 . . . . 5 (𝜑 → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵) ↔ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴))
127, 11mpbird 246 . . . 4 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵))
1312adantr 480 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵))
14 fsovfvd.g . . . 4 𝐺 = (𝐴𝑂𝐵)
15 fsovd.fs . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
1615, 1, 10fsovd 37322 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
1714, 16syl5eq 2656 . . 3 (𝜑𝐺 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
18 fsovcnvlem.h . . . 4 𝐻 = (𝐵𝑂𝐴)
19 oveq2 6557 . . . . . . . 8 (𝑎 = 𝑑 → (𝒫 𝑏𝑚 𝑎) = (𝒫 𝑏𝑚 𝑑))
20 rabeq 3166 . . . . . . . . 9 (𝑎 = 𝑑 → {𝑥𝑎𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑓𝑥)})
2120mpteq2dv 4673 . . . . . . . 8 (𝑎 = 𝑑 → (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2219, 21mpteq12dv 4663 . . . . . . 7 (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑏𝑚 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
23 pweq 4111 . . . . . . . . 9 (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
2423oveq1d 6564 . . . . . . . 8 (𝑏 = 𝑐 → (𝒫 𝑏𝑚 𝑑) = (𝒫 𝑐𝑚 𝑑))
25 mpteq1 4665 . . . . . . . 8 (𝑏 = 𝑐 → (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2624, 25mpteq12dv 4663 . . . . . . 7 (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏𝑚 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
2722, 26cbvmpt2v 6633 . . . . . 6 (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
28 eqid 2610 . . . . . . 7 V = V
29 fveq1 6102 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
3029eleq2d 2673 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑦 ∈ (𝑔𝑥)))
3130rabbidv 3164 . . . . . . . . . 10 (𝑓 = 𝑔 → {𝑥𝑑𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑔𝑥)})
3231mpteq2dv 4673 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
3332cbvmptv 4678 . . . . . . . 8 (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
34 eleq1 2676 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑥)))
3534rabbidv 3164 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑥𝑑𝑦 ∈ (𝑔𝑥)} = {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
3635cbvmptv 4678 . . . . . . . . . 10 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
37 fveq2 6103 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑔𝑥) = (𝑔𝑣))
3837eleq2d 2673 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑢 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑣)))
3938cbvrabv 3172 . . . . . . . . . . 11 {𝑥𝑑𝑢 ∈ (𝑔𝑥)} = {𝑣𝑑𝑢 ∈ (𝑔𝑣)}
4039mpteq2i 4669 . . . . . . . . . 10 (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4136, 40eqtri 2632 . . . . . . . . 9 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4241mpteq2i 4669 . . . . . . . 8 (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4333, 42eqtri 2632 . . . . . . 7 (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4428, 28, 43mpt2eq123i 6616 . . . . . 6 (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4515, 27, 443eqtri 2636 . . . . 5 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4645, 10, 1fsovd 37322 . . . 4 (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴𝑚 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
4718, 46syl5eq 2656 . . 3 (𝜑𝐻 = (𝑔 ∈ (𝒫 𝐴𝑚 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
48 fveq1 6102 . . . . . 6 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑔𝑣) = ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣))
4948eleq2d 2673 . . . . 5 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢 ∈ (𝑔𝑣) ↔ 𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)))
5049rabbidv 3164 . . . 4 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → {𝑣𝐵𝑢 ∈ (𝑔𝑣)} = {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})
5150mpteq2dv 4673 . . 3 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)}) = (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}))
5213, 17, 47, 51fmptco 6303 . 2 (𝜑 → (𝐻𝐺) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})))
53 eqidd 2611 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}))
54 eleq1 2676 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑥)))
5554rabbidv 3164 . . . . . . . . . . . 12 (𝑦 = 𝑣 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
5655adantl 481 . . . . . . . . . . 11 ((((𝜑𝑢𝐴) ∧ 𝑣𝐵) ∧ 𝑦 = 𝑣) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
57 simpr 476 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → 𝑣𝐵)
58 rabexg 4739 . . . . . . . . . . . . 13 (𝐴𝑉 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
591, 58syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
6059ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
6153, 56, 57, 60fvmptd 6197 . . . . . . . . . 10 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
6261eleq2d 2673 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)}))
63 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑓𝑥) = (𝑓𝑢))
6463eleq2d 2673 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑣 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
6564elrab3 3332 . . . . . . . . . 10 (𝑢𝐴 → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6665ad2antlr 759 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6762, 66bitrd 267 . . . . . . . 8 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓𝑢)))
6867rabbidva 3163 . . . . . . 7 ((𝜑𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
6968adantlr 747 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
70 dfin5 3548 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)}
71 elmapi 7765 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
7271ad2antlr 759 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
73 simpr 476 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → 𝑢𝐴)
7472, 73ffvelrnd 6268 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
7574elpwid 4118 . . . . . . . 8 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
76 sseqin2 3779 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7775, 76sylib 207 . . . . . . 7 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7870, 77syl5reqr 2659 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
7969, 78eqtr4d 2647 . . . . 5 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = (𝑓𝑢))
8079mpteq2dva 4672 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = (𝑢𝐴 ↦ (𝑓𝑢)))
8171feqmptd 6159 . . . . 5 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8281adantl 481 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8380, 82eqtr4d 2647 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = 𝑓)
8483mpteq2dva 4672 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓))
85 mptresid 5375 . . 3 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵𝑚 𝐴))
8685a1i 11 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
8752, 84, 863eqtrd 2648 1 (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108   ↦ cmpt 4643   I cid 4948   ↾ cres 5040   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑𝑚 cmap 7744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746 This theorem is referenced by:  fsovcnvd  37328
 Copyright terms: Public domain W3C validator