Theorem fsovcnvlem 43067

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 4078	. . . . . . . . 9 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴
3	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴)
4	1, 3	sselpwd 5327	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴)
5	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴)
6	5	fmpttd 7117	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴)
7	1	pwexd 5378	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
8		fsovd.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
9	7, 8	elmapd 8837	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴))
10	6, 9	mpbird 256	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵))
11	10	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵))
12		fsovfvd.g	. . . 4 ⊢ 𝐺 = (𝐴𝑂𝐵)
13		fsovd.fs	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
14	13, 1, 8	fsovd 43062	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
15	12, 14	eqtrid 2783	. . 3 ⊢ (𝜑 → 𝐺 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
16		fsovcnvlem.h	. . . 4 ⊢ 𝐻 = (𝐵𝑂𝐴)
17		oveq2 7420	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝒫 𝑏 ↑m 𝑎) = (𝒫 𝑏 ↑m 𝑑))
18		rabeq 3445	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})
19	18	mpteq2dv 5251	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
20	17, 19	mpteq12dv 5240	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
21		pweq 4617	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
22	21	oveq1d 7427	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝒫 𝑏 ↑m 𝑑) = (𝒫 𝑐 ↑m 𝑑))
23		mpteq1 5242	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
24	22, 23	mpteq12dv 5240	. . . . . . 7 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
25	20, 24	cbvmpov 7507	. . . . . 6 ⊢ (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
26		eqid 2731	. . . . . . 7 ⊢ V = V
27		fveq1 6891	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
28	27	eleq2d 2818	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑔‘𝑥)))
29	28	rabbidv 3439	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})
30	29	mpteq2dv 5251	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}))
31	30	cbvmptv 5262	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}))
32		eleq1w 2815	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑥)))
33	32	rabbidv 3439	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)})
34	33	cbvmptv 5262	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)})
35		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝑔‘𝑥) = (𝑔‘𝑣))
36	35	eleq2d 2818	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (𝑢 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑣)))
37	36	cbvrabv 3441	. . . . . . . . . . 11 ⊢ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)} = {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}
38	37	mpteq2i 5254	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})
39	34, 38	eqtri 2759	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})
40	39	mpteq2i 5254	. . . . . . . 8 ⊢ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))
41	31, 40	eqtri 2759	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))
42	26, 26, 41	mpoeq123i 7488	. . . . . 6 ⊢ (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
43	13, 25, 42	3eqtri 2763	. . . . 5 ⊢ 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
44	43, 8, 1	fsovd 43062	. . . 4 ⊢ (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
45	16, 44	eqtrid 2783	. . 3 ⊢ (𝜑 → 𝐻 = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
46		fveq1 6891	. . . . . 6 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑔‘𝑣) = ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣))
47	46	eleq2d 2818	. . . . 5 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ (𝑔‘𝑣) ↔ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)))
48	47	rabbidv 3439	. . . 4 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})
49	48	mpteq2dv 5251	. . 3 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}))
50	11, 15, 45, 49	fmptco 7130	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐺) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})))
51		eqidd 2732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
52		eleq1w 2815	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑥)))
53	52	rabbidv 3439	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
54	53	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) ∧ 𝑦 = 𝑣) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
55		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵)
56		rabexg 5332	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
57	1, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
58	57	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
59	51, 54, 55, 58	fvmptd 7006	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
60	59	eleq2d 2818	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}))
61		fveq2 6892	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝑓‘𝑥) = (𝑓‘𝑢))
62	61	eleq2d 2818	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑣 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
63	62	elrab3 3685	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴 → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢)))
64	63	ad2antlr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢)))
65	60, 64	bitrd 278	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓‘𝑢)))
66	65	rabbidva 3438	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
67	66	adantlr 712	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
68		elmapi 8846	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
69	68	ad2antlr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
70		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
71	69, 70	ffvelcdmd 7088	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
72	71	elpwid 4612	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
73		sseqin2 4216	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
74	72, 73	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
75		dfin5 3957	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}
76	74, 75	eqtr3di 2786	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
77	67, 76	eqtr4d 2774	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = (𝑓‘𝑢))
78	77	mpteq2dva 5249	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
79	68	feqmptd 6961	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
80	79	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
81	78, 80	eqtr4d 2774	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = 𝑓)
82	81	mpteq2dva 5249	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓))
83		mptresid 6051	. . . 4 ⊢ ( I ↾ (𝒫 𝐵 ↑m 𝐴)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓)
84	83	eqcomi 2740	. . 3 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴))
85	84	a1i 11	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))
86	50, 82, 85	3eqtrd 2775	1 ⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {crab 3431  Vcvv 3473   ∩ cin 3948   ⊆ wss 3949  𝒫 cpw 4603   ↦ cmpt 5232   I cid 5574   ↾ cres 5679   ∘ ccom 5681  ⟶wf 6540  ‘cfv 6544  (class class class)co 7412   ∈ cmpo 7414   ↑_m cmap 8823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7978  df-2nd 7979  df-map 8825

This theorem is referenced by:  fsovcnvd  43068