Theorem fsovcnvlem 40352

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 ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
fsovd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fsovd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
fsovfvd.g	⊢ 𝐺 = (𝐴𝑂𝐵)
fsovcnvlem.h	⊢ 𝐻 = (𝐵𝑂𝐴)

Assertion

Ref	Expression
fsovcnvlem	⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑥,𝑦   𝐵,𝑎,𝑏,𝑓,𝑦   𝜑,𝑎,𝑏,𝑓,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐺(𝑥,𝑦,𝑓,𝑎,𝑏)   𝐻(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑂(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑊(𝑥,𝑦,𝑓,𝑎,𝑏)

Proof of Theorem fsovcnvlem

Dummy variables 𝑐 𝑑 𝑔 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fsovd.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		ssrab2 4056	. . . . . . . . 9 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴
3	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴)
4	1, 3	sselpwd 5223	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴)
5	4	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴)
6	5	fmpttd 6874	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴)
7	1	pwexd 5273	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
8		fsovd.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
9	7, 8	elmapd 8414	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴))
10	6, 9	mpbird 259	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵))
11	10	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵))
12		fsovfvd.g	. . . 4 ⊢ 𝐺 = (𝐴𝑂𝐵)
13		fsovd.fs	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
14	13, 1, 8	fsovd 40347	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
15	12, 14	syl5eq 2868	. . 3 ⊢ (𝜑 → 𝐺 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
16		fsovcnvlem.h	. . . 4 ⊢ 𝐻 = (𝐵𝑂𝐴)
17		oveq2 7158	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝒫 𝑏 ↑m 𝑎) = (𝒫 𝑏 ↑m 𝑑))
18		rabeq 3484	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})
19	18	mpteq2dv 5155	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
20	17, 19	mpteq12dv 5144	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
21		pweq 4542	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
22	21	oveq1d 7165	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝒫 𝑏 ↑m 𝑑) = (𝒫 𝑐 ↑m 𝑑))
23		mpteq1 5147	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
24	22, 23	mpteq12dv 5144	. . . . . . 7 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
25	20, 24	cbvmpov 7243	. . . . . 6 ⊢ (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
26		eqid 2821	. . . . . . 7 ⊢ V = V
27		fveq1 6664	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
28	27	eleq2d 2898	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑔‘𝑥)))
29	28	rabbidv 3481	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})
30	29	mpteq2dv 5155	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}))
31	30	cbvmptv 5162	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}))
32		eleq1w 2895	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑥)))
33	32	rabbidv 3481	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)})
34	33	cbvmptv 5162	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)})
35		fveq2 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝑔‘𝑥) = (𝑔‘𝑣))
36	35	eleq2d 2898	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (𝑢 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑣)))
37	36	cbvrabv 3492	. . . . . . . . . . 11 ⊢ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)} = {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}
38	37	mpteq2i 5151	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})
39	34, 38	eqtri 2844	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})
40	39	mpteq2i 5151	. . . . . . . 8 ⊢ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))
41	31, 40	eqtri 2844	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))
42	26, 26, 41	mpoeq123i 7224	. . . . . 6 ⊢ (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
43	13, 25, 42	3eqtri 2848	. . . . 5 ⊢ 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
44	43, 8, 1	fsovd 40347	. . . 4 ⊢ (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
45	16, 44	syl5eq 2868	. . 3 ⊢ (𝜑 → 𝐻 = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
46		fveq1 6664	. . . . . 6 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑔‘𝑣) = ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣))
47	46	eleq2d 2898	. . . . 5 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ (𝑔‘𝑣) ↔ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)))
48	47	rabbidv 3481	. . . 4 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})
49	48	mpteq2dv 5155	. . 3 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}))
50	11, 15, 45, 49	fmptco 6886	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐺) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})))
51		eqidd 2822	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
52		eleq1w 2895	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑥)))
53	52	rabbidv 3481	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
54	53	adantl 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) ∧ 𝑦 = 𝑣) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
55		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵)
56		rabexg 5227	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
57	1, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
58	57	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
59	51, 54, 55, 58	fvmptd 6770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
60	59	eleq2d 2898	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}))
61		fveq2 6665	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝑓‘𝑥) = (𝑓‘𝑢))
62	61	eleq2d 2898	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑣 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
63	62	elrab3 3681	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴 → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢)))
64	63	ad2antlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢)))
65	60, 64	bitrd 281	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓‘𝑢)))
66	65	rabbidva 3479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
67	66	adantlr 713	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
68		dfin5 3944	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}
69		elmapi 8422	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
70	69	ad2antlr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
71		simpr 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
72	70, 71	ffvelrnd 6847	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
73	72	elpwid 4553	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
74		sseqin2 4192	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
75	73, 74	sylib 220	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
76	68, 75	syl5reqr 2871	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
77	67, 76	eqtr4d 2859	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = (𝑓‘𝑢))
78	77	mpteq2dva 5154	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
79	69	feqmptd 6728	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
80	79	adantl 484	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
81	78, 80	eqtr4d 2859	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = 𝑓)
82	81	mpteq2dva 5154	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓))
83		mptresid 5913	. . . 4 ⊢ ( I ↾ (𝒫 𝐵 ↑m 𝐴)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓)
84	83	eqcomi 2830	. . 3 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴))
85	84	a1i 11	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))
86	50, 82, 85	3eqtrd 2860	1 ⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {crab 3142  Vcvv 3495   ∩ cin 3935   ⊆ wss 3936  𝒫 cpw 4539   ↦ cmpt 5139   I cid 5454   ↾ cres 5552   ∘ ccom 5554  ⟶wf 6346  ‘cfv 6350  (class class class)co 7150   ∈ cmpo 7152   ↑_m cmap 8400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-map 8402

This theorem is referenced by:  fsovcnvd  40353