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

Theorem fsovcnvlem 38828
 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 3829 . . . . . . . . 9 {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴
32a1i 11 . . . . . . . 8 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴)
41, 3sselpwd 4960 . . . . . . 7 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
54adantr 472 . . . . . 6 ((𝜑𝑦𝐵) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
6 eqid 2761 . . . . . 6 (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})
75, 6fmptd 6550 . . . . 5 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴)
8 pwexg 5000 . . . . . . 7 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
91, 8syl 17 . . . . . 6 (𝜑 → 𝒫 𝐴 ∈ V)
10 fsovd.b . . . . . 6 (𝜑𝐵𝑊)
119, 10elmapd 8040 . . . . 5 (𝜑 → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵) ↔ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴))
127, 11mpbird 247 . . . 4 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵))
1312adantr 472 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵))
14 fsovfvd.g . . . 4 𝐺 = (𝐴𝑂𝐵)
15 fsovd.fs . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
1615, 1, 10fsovd 38823 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
1714, 16syl5eq 2807 . . 3 (𝜑𝐺 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
18 fsovcnvlem.h . . . 4 𝐻 = (𝐵𝑂𝐴)
19 oveq2 6823 . . . . . . . 8 (𝑎 = 𝑑 → (𝒫 𝑏𝑚 𝑎) = (𝒫 𝑏𝑚 𝑑))
20 rabeq 3333 . . . . . . . . 9 (𝑎 = 𝑑 → {𝑥𝑎𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑓𝑥)})
2120mpteq2dv 4898 . . . . . . . 8 (𝑎 = 𝑑 → (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2219, 21mpteq12dv 4886 . . . . . . 7 (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑏𝑚 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
23 pweq 4306 . . . . . . . . 9 (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
2423oveq1d 6830 . . . . . . . 8 (𝑏 = 𝑐 → (𝒫 𝑏𝑚 𝑑) = (𝒫 𝑐𝑚 𝑑))
25 mpteq1 4890 . . . . . . . 8 (𝑏 = 𝑐 → (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2624, 25mpteq12dv 4886 . . . . . . 7 (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏𝑚 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
2722, 26cbvmpt2v 6902 . . . . . 6 (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
28 eqid 2761 . . . . . . 7 V = V
29 fveq1 6353 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
3029eleq2d 2826 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑦 ∈ (𝑔𝑥)))
3130rabbidv 3330 . . . . . . . . . 10 (𝑓 = 𝑔 → {𝑥𝑑𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑔𝑥)})
3231mpteq2dv 4898 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
3332cbvmptv 4903 . . . . . . . 8 (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
34 eleq1w 2823 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑥)))
3534rabbidv 3330 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑥𝑑𝑦 ∈ (𝑔𝑥)} = {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
3635cbvmptv 4903 . . . . . . . . . 10 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
37 fveq2 6354 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑔𝑥) = (𝑔𝑣))
3837eleq2d 2826 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑢 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑣)))
3938cbvrabv 3340 . . . . . . . . . . 11 {𝑥𝑑𝑢 ∈ (𝑔𝑥)} = {𝑣𝑑𝑢 ∈ (𝑔𝑣)}
4039mpteq2i 4894 . . . . . . . . . 10 (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4136, 40eqtri 2783 . . . . . . . . 9 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4241mpteq2i 4894 . . . . . . . 8 (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4333, 42eqtri 2783 . . . . . . 7 (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4428, 28, 43mpt2eq123i 6885 . . . . . 6 (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4515, 27, 443eqtri 2787 . . . . 5 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4645, 10, 1fsovd 38823 . . . 4 (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴𝑚 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
4718, 46syl5eq 2807 . . 3 (𝜑𝐻 = (𝑔 ∈ (𝒫 𝐴𝑚 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
48 fveq1 6353 . . . . . 6 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑔𝑣) = ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣))
4948eleq2d 2826 . . . . 5 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢 ∈ (𝑔𝑣) ↔ 𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)))
5049rabbidv 3330 . . . 4 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → {𝑣𝐵𝑢 ∈ (𝑔𝑣)} = {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})
5150mpteq2dv 4898 . . 3 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)}) = (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}))
5213, 17, 47, 51fmptco 6561 . 2 (𝜑 → (𝐻𝐺) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})))
53 eqidd 2762 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}))
54 eleq1w 2823 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑥)))
5554rabbidv 3330 . . . . . . . . . . . 12 (𝑦 = 𝑣 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
5655adantl 473 . . . . . . . . . . 11 ((((𝜑𝑢𝐴) ∧ 𝑣𝐵) ∧ 𝑦 = 𝑣) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
57 simpr 479 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → 𝑣𝐵)
58 rabexg 4964 . . . . . . . . . . . . 13 (𝐴𝑉 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
591, 58syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
6059ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
6153, 56, 57, 60fvmptd 6452 . . . . . . . . . 10 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
6261eleq2d 2826 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)}))
63 fveq2 6354 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑓𝑥) = (𝑓𝑢))
6463eleq2d 2826 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑣 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
6564elrab3 3506 . . . . . . . . . 10 (𝑢𝐴 → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6665ad2antlr 765 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6762, 66bitrd 268 . . . . . . . 8 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓𝑢)))
6867rabbidva 3329 . . . . . . 7 ((𝜑𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
6968adantlr 753 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
70 dfin5 3724 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)}
71 elmapi 8048 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
7271ad2antlr 765 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
73 simpr 479 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → 𝑢𝐴)
7472, 73ffvelrnd 6525 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
7574elpwid 4315 . . . . . . . 8 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
76 sseqin2 3961 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7775, 76sylib 208 . . . . . . 7 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7870, 77syl5reqr 2810 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
7969, 78eqtr4d 2798 . . . . 5 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = (𝑓𝑢))
8079mpteq2dva 4897 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = (𝑢𝐴 ↦ (𝑓𝑢)))
8171feqmptd 6413 . . . . 5 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8281adantl 473 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8380, 82eqtr4d 2798 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = 𝑓)
8483mpteq2dva 4897 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓))
85 mptresid 5615 . . 3 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵𝑚 𝐴))
8685a1i 11 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
8752, 84, 863eqtrd 2799 1 (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2140  {crab 3055  Vcvv 3341   ∩ cin 3715   ⊆ wss 3716  𝒫 cpw 4303   ↦ cmpt 4882   I cid 5174   ↾ cres 5269   ∘ ccom 5271  ⟶wf 6046  ‘cfv 6050  (class class class)co 6815   ↦ cmpt2 6817   ↑𝑚 cmap 8026 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-1st 7335  df-2nd 7336  df-map 8028 This theorem is referenced by:  fsovcnvd  38829
 Copyright terms: Public domain W3C validator