Theorem fsovrfovd 43676

Description: The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021.)

Hypotheses

Ref	Expression
fsovd.fs	⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
fsovd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fsovd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
fsovd.rf	⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣})))
fsovd.cnv	⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠))

Assertion

Ref	Expression
fsovrfovd	⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑟,𝑢,𝑣   𝐴,𝑠,𝑎,𝑏,𝑓,𝑢,𝑣   𝑥,𝐴,𝑦,𝑎,𝑏,𝑓   𝐵,𝑎,𝑏,𝑓,𝑟,𝑢,𝑣   𝐵,𝑠   𝑦,𝐵   𝑊,𝑎,𝑢   𝜑,𝑎,𝑏,𝑓,𝑟,𝑢,𝑣

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑠)   𝐵(𝑥)   𝐶(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑅(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑂(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑣,𝑢,𝑓,𝑠,𝑟,𝑎,𝑏)   𝑊(𝑥,𝑦,𝑣,𝑓,𝑠,𝑟,𝑏)

Proof of Theorem fsovrfovd

Dummy variables 𝑐 𝑑 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fsovd.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
2		fsovd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	1, 2	xpexd 7759	. . . . 5 ⊢ (𝜑 → (𝐵 × 𝐴) ∈ V)
4	3	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐵 × 𝐴) ∈ V)
5		elmapi 8878	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6	5	ffvelcdmda 7098	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
7	6	elpwid 4616	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
8	7	sseld 3978	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → 𝑣 ∈ 𝐵))
9	8	impancom 450	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 → 𝑣 ∈ 𝐵))
10	9	pm4.71d 560	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)))
11	10	ex 411	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵))))
12	11	pm5.32rd 576	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))))
13		ancom 459	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ↔ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴))
14	13	anbi1i 622	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)))
15	12, 14	bitrdi 286	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))))
16	15	opabbidv 5219	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑣, 𝑢⟩ ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))})
17		opabssxp 5774	. . . . . 6 ⊢ {⟨𝑣, 𝑢⟩ ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)
18	16, 17	eqsstrdi 4034	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴))
19	18	adantl 480	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴))
20	4, 19	sselpwd 5333	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐵 × 𝐴))
21		eqidd 2727	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
22		fsovd.rf	. . . . 5 ⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣})))
23	22, 1, 2	rfovd 43668	. . . 4 ⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})))
24		breq 5155	. . . . . . . 8 ⊢ (𝑟 = 𝑡 → (𝑢𝑟𝑣 ↔ 𝑢𝑡𝑣))
25	24	rabbidv 3427	. . . . . . 7 ⊢ (𝑟 = 𝑡 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣})
26	25	mpteq2dv 5255	. . . . . 6 ⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}))
27		breq1 5156	. . . . . . . . 9 ⊢ (𝑢 = 𝑐 → (𝑢𝑡𝑣 ↔ 𝑐𝑡𝑣))
28	27	rabbidv 3427	. . . . . . . 8 ⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣})
29		breq2 5157	. . . . . . . . 9 ⊢ (𝑣 = 𝑑 → (𝑐𝑡𝑣 ↔ 𝑐𝑡𝑑))
30	29	cbvrabv 3430	. . . . . . . 8 ⊢ {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}
31	28, 30	eqtrdi 2782	. . . . . . 7 ⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})
32	31	cbvmptv 5266	. . . . . 6 ⊢ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})
33	26, 32	eqtrdi 2782	. . . . 5 ⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))
34	33	cbvmptv 5266	. . . 4 ⊢ (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))
35	23, 34	eqtrdi 2782	. . 3 ⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})))
36		breq 5155	. . . . . . 7 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ 𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑))
37		df-br 5154	. . . . . . . 8 ⊢ (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
38		vex 3466	. . . . . . . . 9 ⊢ 𝑐 ∈ V
39		vex 3466	. . . . . . . . 9 ⊢ 𝑑 ∈ V
40		eleq1w 2809	. . . . . . . . . 10 ⊢ (𝑣 = 𝑐 → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑢)))
41	40	anbi2d 628	. . . . . . . . 9 ⊢ (𝑣 = 𝑐 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢))))
42		eleq1w 2809	. . . . . . . . . 10 ⊢ (𝑢 = 𝑑 → (𝑢 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴))
43		fveq2 6901	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑑 → (𝑓‘𝑢) = (𝑓‘𝑑))
44	43	eleq2d 2812	. . . . . . . . . 10 ⊢ (𝑢 = 𝑑 → (𝑐 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑑)))
45	42, 44	anbi12d 630	. . . . . . . . 9 ⊢ (𝑢 = 𝑑 → ((𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
46	38, 39, 41, 45	opelopab 5548	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))
47	37, 46	bitri 274	. . . . . . 7 ⊢ (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))
48	36, 47	bitrdi 286	. . . . . 6 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
49	48	rabbidv 3427	. . . . 5 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))})
50	49	mpteq2dv 5255	. . . 4 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}))
51		ibar 527	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝐴 → (𝑐 ∈ (𝑓‘𝑑) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
52	51	bicomd 222	. . . . . . . 8 ⊢ (𝑑 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)) ↔ 𝑐 ∈ (𝑓‘𝑑)))
53	52	rabbiia 3423	. . . . . . 7 ⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)}
54		fveq2 6901	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → (𝑓‘𝑑) = (𝑓‘𝑥))
55	54	eleq2d 2812	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑐 ∈ (𝑓‘𝑑) ↔ 𝑐 ∈ (𝑓‘𝑥)))
56	55	cbvrabv 3430	. . . . . . 7 ⊢ {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}
57	53, 56	eqtri 2754	. . . . . 6 ⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}
58	57	mpteq2i 5258	. . . . 5 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)})
59		eleq1w 2809	. . . . . . 7 ⊢ (𝑐 = 𝑦 → (𝑐 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑓‘𝑥)))
60	59	rabbidv 3427	. . . . . 6 ⊢ (𝑐 = 𝑦 → {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
61	60	cbvmptv 5266	. . . . 5 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
62	58, 61	eqtri 2754	. . . 4 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
63	50, 62	eqtrdi 2782	. . 3 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
64	20, 21, 35, 63	fmptco 7143	. 2 ⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
65	2, 1	xpexd 7759	. . . . . 6 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
66	65	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V)
67	12	opabbidv 5219	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))})
68		opabssxp 5774	. . . . . . 7 ⊢ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)
69	67, 68	eqsstrdi 4034	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵))
70	69	adantl 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵))
71	66, 70	sselpwd 5333	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐴 × 𝐵))
72		eqid 2726	. . . . 5 ⊢ (𝐴𝑅𝐵) = (𝐴𝑅𝐵)
73	22, 2, 1, 72	rfovcnvd 43672	. . . 4 ⊢ (𝜑 → ◡(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
74		fsovd.cnv	. . . . . 6 ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠))
75	74	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠)))
76		xpeq12 5707	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 × 𝑏) = (𝐴 × 𝐵))
77	76	pweqd 4624	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝐵))
78	77	mpteq1d 5248	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
79	78	adantl 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
80	2	elexd 3485	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
81	1	elexd 3485	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
82		pwexg 5382	. . . . . 6 ⊢ ((𝐴 × 𝐵) ∈ V → 𝒫 (𝐴 × 𝐵) ∈ V)
83		mptexg 7238	. . . . . 6 ⊢ (𝒫 (𝐴 × 𝐵) ∈ V → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V)
84	65, 82, 83	3syl 18	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V)
85	75, 79, 80, 81, 84	ovmpod 7578	. . . 4 ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
86		cnveq 5880	. . . . 5 ⊢ (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = ◡{⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
87		cnvopab 6149	. . . . 5 ⊢ ◡{⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}
88	86, 87	eqtrdi 2782	. . . 4 ⊢ (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
89	71, 73, 85, 88	fmptco 7143	. . 3 ⊢ (𝜑 → ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
90	89	coeq2d 5869	. 2 ⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))) = ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})))
91		fsovd.fs	. . 3 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
92	91, 2, 1	fsovd 43675	. 2 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
93	64, 90, 92	3eqtr4rd 2777	1 ⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  {crab 3419  Vcvv 3462   ⊆ wss 3947  𝒫 cpw 4607  ⟨cop 4639   class class class wbr 5153  {copab 5215   ↦ cmpt 5236   × cxp 5680  ^◡ccnv 5681   ∘ ccom 5686  ‘cfv 6554  (class class class)co 7424   ∈ cmpo 7426   ↑_m cmap 8855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8003  df-2nd 8004  df-map 8857

This theorem is referenced by: (None)