Theorem fsovcnvlem 45159

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 4008	. . . . . . . . 9 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴
3	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐴)
4	1, 3	sselpwd 5294	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴)
5	4	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ 𝒫 𝐴)
6	5	fmpttd 7126	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴)
7	1	pwexd 5345	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
8		fsovd.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
9	7, 8	elmapd 8874	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}):𝐵⟶𝒫 𝐴))
10	6, 9	mpbird 260	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵))
11	10	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) ∈ (𝒫 𝐴 ↑m 𝐵))
12		fsovfvd.g	. . . 4 ⊢ 𝐺 = (𝐴𝑂𝐵)
13		fsovd.fs	. . . . 5 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
14	13, 1, 8	fsovd 45154	. . . 4 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
15	12, 14	eqtrid 2810	. . 3 ⊢ (𝜑 → 𝐺 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
16		fsovcnvlem.h	. . . 4 ⊢ 𝐻 = (𝐵𝑂𝐴)
17		oveq2 7438	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝒫 𝑏 ↑m 𝑎) = (𝒫 𝑏 ↑m 𝑑))
18		rabeq 3430	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})
19	18	mpteq2dv 5202	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
20	17, 19	mpteq12dv 5195	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
21		pweq 4574	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
22	21	oveq1d 7445	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝒫 𝑏 ↑m 𝑑) = (𝒫 𝑐 ↑m 𝑑))
23		mpteq1 5197	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
24	22, 23	mpteq12dv 5195	. . . . . . 7 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑑) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
25	20, 24	cbvmpov 7525	. . . . . 6 ⊢ (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
26		eqid 2763	. . . . . . 7 ⊢ V = V
27		fveq1 6895	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
28	27	eleq2d 2850	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑔‘𝑥)))
29	28	rabbidv 3423	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})
30	29	mpteq2dv 5202	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}))
31	30	cbvmptv 5212	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}))
32		eleq1w 2847	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑥)))
33	32	rabbidv 3423	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)} = {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)})
34	33	cbvmptv 5212	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)})
35		fveq2 6896	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝑔‘𝑥) = (𝑔‘𝑣))
36	35	eleq2d 2850	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (𝑢 ∈ (𝑔‘𝑥) ↔ 𝑢 ∈ (𝑔‘𝑣)))
37	36	cbvrabv 3426	. . . . . . . . . . 11 ⊢ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)} = {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}
38	37	mpteq2i 5204	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})
39	34, 38	eqtri 2786	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)}) = (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})
40	39	mpteq2i 5204	. . . . . . . 8 ⊢ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑔‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))
41	31, 40	eqtri 2786	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)}))
42	26, 26, 41	mpoeq123i 7506	. . . . . 6 ⊢ (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑦 ∈ 𝑐 ↦ {𝑥 ∈ 𝑑 ∣ 𝑦 ∈ (𝑓‘𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
43	13, 25, 42	3eqtri 2790	. . . . 5 ⊢ 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐 ↑m 𝑑) ↦ (𝑢 ∈ 𝑐 ↦ {𝑣 ∈ 𝑑 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
44	43, 8, 1	fsovd 45154	. . . 4 ⊢ (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
45	16, 44	eqtrid 2810	. . 3 ⊢ (𝜑 → 𝐻 = (𝑔 ∈ (𝒫 𝐴 ↑m 𝐵) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)})))
46		fveq1 6895	. . . . . 6 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑔‘𝑣) = ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣))
47	46	eleq2d 2850	. . . . 5 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ (𝑔‘𝑣) ↔ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)))
48	47	rabbidv 3423	. . . 4 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})
49	48	mpteq2dv 5202	. . 3 ⊢ (𝑔 = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ (𝑔‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}))
50	11, 15, 45, 49	fmptco 7141	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐺) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})))
51		eqidd 2764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
52		eleq1w 2847	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑥)))
53	52	rabbidv 3423	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
54	53	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) ∧ 𝑦 = 𝑣) → {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
55		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵)
56		rabexg 5303	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
57	1, 56	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
58	57	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ∈ V)
59	51, 54, 55, 58	fvmptd 7012	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) = {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)})
60	59	eleq2d 2850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)}))
61		fveq2 6896	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝑓‘𝑥) = (𝑓‘𝑢))
62	61	eleq2d 2850	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑣 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢)))
63	62	elrab3 3649	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴 → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢)))
64	63	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑣 ∈ (𝑓‘𝑥)} ↔ 𝑣 ∈ (𝑓‘𝑢)))
65	60, 64	bitrd 282	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ 𝐵) → (𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓‘𝑢)))
66	65	rabbidva 3422	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
67	66	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
68		elmapi 8883	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
69	68	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
70		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
71	69, 70	ffvelcdmd 7096	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
72	71	elpwid 4569	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
73		sseqin2 4123	. . . . . . . 8 ⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
74	72, 73	sylib 221	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢))
75		dfin5 4095	. . . . . . 7 ⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)}
76	74, 75	eqtr3di 2813	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑣 ∈ 𝐵 ∣ 𝑣 ∈ (𝑓‘𝑢)})
77	67, 76	eqtr4d 2801	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) ∧ 𝑢 ∈ 𝐴) → {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)} = (𝑓‘𝑢))
78	77	mpteq2dva 5201	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
79	68	feqmptd 6964	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
80	79	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → 𝑓 = (𝑢 ∈ 𝐴 ↦ (𝑓‘𝑢)))
81	78, 80	eqtr4d 2801	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)}) = 𝑓)
82	81	mpteq2dva 5201	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑢 ∈ 𝐴 ↦ {𝑣 ∈ 𝐵 ∣ 𝑢 ∈ ((𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓))
83		mptresid 6049	. . . 4 ⊢ ( I ↾ (𝒫 𝐵 ↑m 𝐴)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓)
84	83	eqcomi 2772	. . 3 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴))
85	84	a1i 11	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))
86	50, 82, 85	3eqtrd 2802	1 ⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑m 𝐴)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  𝒫 cpw 4560   ↦ cmpt 5189   I cid 5549   ↾ cres 5657   ∘ ccom 5659  ⟶wf 6543  ‘cfv 6547  (class class class)co 7430   ∈ cmpo 7432   ↑_m cmap 8861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8011  df-2nd 8012  df-map 8863

This theorem is used by:  fsovcnvd  45160