Theorem fsovrfovd 44453

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 7694	. . . . 5 ⊢ (𝜑 → (𝐵 × 𝐴) ∈ V)
4	3	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐵 × 𝐴) ∈ V)
5		elmapi 8786	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6	5	ffvelcdmda 7025	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
7	6	elpwid 4538	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
8	7	sseld 3914	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → 𝑣 ∈ 𝐵))
9	8	impancom 452	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 → 𝑣 ∈ 𝐵))
10	9	pm4.71d 566	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)))
11	10	ex 413	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵))))
12	11	pm5.32rd 583	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))))
13		ancom 461	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ↔ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴))
14	13	anbi1i 630	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)))
15	12, 14	bitrdi 288	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))))
16	15	opabbidv 5138	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑣, 𝑢⟩ ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))})
17		opabssxp 5710	. . . . . 6 ⊢ {⟨𝑣, 𝑢⟩ ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)
18	16, 17	eqsstrdi 3959	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴))
19	18	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴))
20	4, 19	sselpwd 5256	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐵 × 𝐴))
21		eqidd 2740	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
22		fsovd.rf	. . . . 5 ⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣})))
23	22, 1, 2	rfovd 44445	. . . 4 ⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})))
24		breq 5074	. . . . . . . 8 ⊢ (𝑟 = 𝑡 → (𝑢𝑟𝑣 ↔ 𝑢𝑡𝑣))
25	24	rabbidv 3398	. . . . . . 7 ⊢ (𝑟 = 𝑡 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣})
26	25	mpteq2dv 5166	. . . . . 6 ⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}))
27		breq1 5075	. . . . . . . . 9 ⊢ (𝑢 = 𝑐 → (𝑢𝑡𝑣 ↔ 𝑐𝑡𝑣))
28	27	rabbidv 3398	. . . . . . . 8 ⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣})
29		breq2 5076	. . . . . . . . 9 ⊢ (𝑣 = 𝑑 → (𝑐𝑡𝑣 ↔ 𝑐𝑡𝑑))
30	29	cbvrabv 3401	. . . . . . . 8 ⊢ {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}
31	28, 30	eqtrdi 2790	. . . . . . 7 ⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})
32	31	cbvmptv 5176	. . . . . 6 ⊢ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})
33	26, 32	eqtrdi 2790	. . . . 5 ⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))
34	33	cbvmptv 5176	. . . 4 ⊢ (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))
35	23, 34	eqtrdi 2790	. . 3 ⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})))
36		breq 5074	. . . . . . 7 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ 𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑))
37		df-br 5073	. . . . . . . 8 ⊢ (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
38		vex 3435	. . . . . . . . 9 ⊢ 𝑐 ∈ V
39		vex 3435	. . . . . . . . 9 ⊢ 𝑑 ∈ V
40		eleq1w 2822	. . . . . . . . . 10 ⊢ (𝑣 = 𝑐 → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑢)))
41	40	anbi2d 636	. . . . . . . . 9 ⊢ (𝑣 = 𝑐 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢))))
42		eleq1w 2822	. . . . . . . . . 10 ⊢ (𝑢 = 𝑑 → (𝑢 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴))
43		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑑 → (𝑓‘𝑢) = (𝑓‘𝑑))
44	43	eleq2d 2825	. . . . . . . . . 10 ⊢ (𝑢 = 𝑑 → (𝑐 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑑)))
45	42, 44	anbi12d 638	. . . . . . . . 9 ⊢ (𝑢 = 𝑑 → ((𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
46	38, 39, 41, 45	opelopab 5484	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))
47	37, 46	bitri 276	. . . . . . 7 ⊢ (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))
48	36, 47	bitrdi 288	. . . . . 6 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
49	48	rabbidv 3398	. . . . 5 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))})
50	49	mpteq2dv 5166	. . . 4 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}))
51		ibar 533	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝐴 → (𝑐 ∈ (𝑓‘𝑑) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
52	51	bicomd 224	. . . . . . . 8 ⊢ (𝑑 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)) ↔ 𝑐 ∈ (𝑓‘𝑑)))
53	52	rabbiia 3395	. . . . . . 7 ⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)}
54		fveq2 6827	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → (𝑓‘𝑑) = (𝑓‘𝑥))
55	54	eleq2d 2825	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑐 ∈ (𝑓‘𝑑) ↔ 𝑐 ∈ (𝑓‘𝑥)))
56	55	cbvrabv 3401	. . . . . . 7 ⊢ {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}
57	53, 56	eqtri 2762	. . . . . 6 ⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}
58	57	mpteq2i 5168	. . . . 5 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)})
59		eleq1w 2822	. . . . . . 7 ⊢ (𝑐 = 𝑦 → (𝑐 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑓‘𝑥)))
60	59	rabbidv 3398	. . . . . 6 ⊢ (𝑐 = 𝑦 → {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
61	60	cbvmptv 5176	. . . . 5 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
62	58, 61	eqtri 2762	. . . 4 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
63	50, 62	eqtrdi 2790	. . 3 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
64	20, 21, 35, 63	fmptco 7071	. 2 ⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
65	2, 1	xpexd 7694	. . . . . 6 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
66	65	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V)
67	12	opabbidv 5138	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))})
68		opabssxp 5710	. . . . . . 7 ⊢ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)
69	67, 68	eqsstrdi 3959	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵))
70	69	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵))
71	66, 70	sselpwd 5256	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐴 × 𝐵))
72		eqid 2739	. . . . 5 ⊢ (𝐴𝑅𝐵) = (𝐴𝑅𝐵)
73	22, 2, 1, 72	rfovcnvd 44449	. . . 4 ⊢ (𝜑 → ◡(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
74		fsovd.cnv	. . . . . 6 ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠))
75	74	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠)))
76		xpeq12 5643	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 × 𝑏) = (𝐴 × 𝐵))
77	76	pweqd 4546	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝐵))
78	77	mpteq1d 5162	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
79	78	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
80	2	elexd 3454	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
81	1	elexd 3454	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
82		pwexg 5307	. . . . . 6 ⊢ ((𝐴 × 𝐵) ∈ V → 𝒫 (𝐴 × 𝐵) ∈ V)
83		mptexg 7165	. . . . . 6 ⊢ (𝒫 (𝐴 × 𝐵) ∈ V → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V)
84	65, 82, 83	3syl 18	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V)
85	75, 79, 80, 81, 84	ovmpod 7508	. . . 4 ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
86		cnveq 5815	. . . . 5 ⊢ (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = ◡{⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
87		cnvopab 6087	. . . . 5 ⊢ ◡{⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}
88	86, 87	eqtrdi 2790	. . . 4 ⊢ (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
89	71, 73, 85, 88	fmptco 7071	. . 3 ⊢ (𝜑 → ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
90	89	coeq2d 5804	. 2 ⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))) = ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})))
91		fsovd.fs	. . 3 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
92	91, 2, 1	fsovd 44452	. 2 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
93	64, 90, 92	3eqtr4rd 2785	1 ⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {crab 3391  Vcvv 3431   ⊆ wss 3883  𝒫 cpw 4529  ⟨cop 4561   class class class wbr 5072  {copab 5134   ↦ cmpt 5153   × cxp 5616  ^◡ccnv 5617   ∘ ccom 5622  ‘cfv 6485  (class class class)co 7356   ∈ cmpo 7358   ↑_m cmap 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-map 8765

This theorem is referenced by: (None)