Theorem fsovrfovd 42271

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 7685	. . . . 5 ⊢ (𝜑 → (𝐵 × 𝐴) ∈ V)
4	3	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐵 × 𝐴) ∈ V)
5		elmapi 8787	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6	5	ffvelcdmda 7035	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵)
7	6	elpwid 4569	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵)
8	7	sseld 3943	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → 𝑣 ∈ 𝐵))
9	8	impancom 452	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 → 𝑣 ∈ 𝐵))
10	9	pm4.71d 562	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)))
11	10	ex 413	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑣 ∈ (𝑓‘𝑢) → (𝑢 ∈ 𝐴 ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵))))
12	11	pm5.32rd 578	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))))
13		ancom 461	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ↔ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴))
14	13	anbi1i 624	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢)))
15	12, 14	bitrdi 286	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))))
16	15	opabbidv 5171	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑣, 𝑢⟩ ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))})
17		opabssxp 5724	. . . . . 6 ⊢ {⟨𝑣, 𝑢⟩ ∣ ((𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴)
18	16, 17	eqsstrdi 3998	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴))
19	18	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐵 × 𝐴))
20	4, 19	sselpwd 5283	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐵 × 𝐴))
21		eqidd 2737	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
22		fsovd.rf	. . . . 5 ⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣})))
23	22, 1, 2	rfovd 42263	. . . 4 ⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})))
24		breq 5107	. . . . . . . 8 ⊢ (𝑟 = 𝑡 → (𝑢𝑟𝑣 ↔ 𝑢𝑡𝑣))
25	24	rabbidv 3415	. . . . . . 7 ⊢ (𝑟 = 𝑡 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣})
26	25	mpteq2dv 5207	. . . . . 6 ⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}))
27		breq1 5108	. . . . . . . . 9 ⊢ (𝑢 = 𝑐 → (𝑢𝑡𝑣 ↔ 𝑐𝑡𝑣))
28	27	rabbidv 3415	. . . . . . . 8 ⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣})
29		breq2 5109	. . . . . . . . 9 ⊢ (𝑣 = 𝑑 → (𝑐𝑡𝑣 ↔ 𝑐𝑡𝑑))
30	29	cbvrabv 3417	. . . . . . . 8 ⊢ {𝑣 ∈ 𝐴 ∣ 𝑐𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}
31	28, 30	eqtrdi 2792	. . . . . . 7 ⊢ (𝑢 = 𝑐 → {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})
32	31	cbvmptv 5218	. . . . . 6 ⊢ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑡𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})
33	26, 32	eqtrdi 2792	. . . . 5 ⊢ (𝑟 = 𝑡 → (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))
34	33	cbvmptv 5218	. . . 4 ⊢ (𝑟 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑢 ∈ 𝐵 ↦ {𝑣 ∈ 𝐴 ∣ 𝑢𝑟𝑣})) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}))
35	23, 34	eqtrdi 2792	. . 3 ⊢ (𝜑 → (𝐵𝑅𝐴) = (𝑡 ∈ 𝒫 (𝐵 × 𝐴) ↦ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑})))
36		breq 5107	. . . . . . 7 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ 𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑))
37		df-br 5106	. . . . . . . 8 ⊢ (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
38		vex 3449	. . . . . . . . 9 ⊢ 𝑐 ∈ V
39		vex 3449	. . . . . . . . 9 ⊢ 𝑑 ∈ V
40		eleq1w 2820	. . . . . . . . . 10 ⊢ (𝑣 = 𝑐 → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑢)))
41	40	anbi2d 629	. . . . . . . . 9 ⊢ (𝑣 = 𝑐 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢))))
42		eleq1w 2820	. . . . . . . . . 10 ⊢ (𝑢 = 𝑑 → (𝑢 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴))
43		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑑 → (𝑓‘𝑢) = (𝑓‘𝑑))
44	43	eleq2d 2823	. . . . . . . . . 10 ⊢ (𝑢 = 𝑑 → (𝑐 ∈ (𝑓‘𝑢) ↔ 𝑐 ∈ (𝑓‘𝑑)))
45	42, 44	anbi12d 631	. . . . . . . . 9 ⊢ (𝑢 = 𝑑 → ((𝑢 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑢)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
46	38, 39, 41, 45	opelopab 5499	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))
47	37, 46	bitri 274	. . . . . . 7 ⊢ (𝑐{⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)))
48	36, 47	bitrdi 286	. . . . . 6 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐𝑡𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
49	48	rabbidv 3415	. . . . 5 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))})
50	49	mpteq2dv 5207	. . . 4 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}))
51		ibar 529	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝐴 → (𝑐 ∈ (𝑓‘𝑑) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))))
52	51	bicomd 222	. . . . . . . 8 ⊢ (𝑑 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑)) ↔ 𝑐 ∈ (𝑓‘𝑑)))
53	52	rabbiia 3411	. . . . . . 7 ⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)}
54		fveq2 6842	. . . . . . . . 9 ⊢ (𝑑 = 𝑥 → (𝑓‘𝑑) = (𝑓‘𝑥))
55	54	eleq2d 2823	. . . . . . . 8 ⊢ (𝑑 = 𝑥 → (𝑐 ∈ (𝑓‘𝑑) ↔ 𝑐 ∈ (𝑓‘𝑥)))
56	55	cbvrabv 3417	. . . . . . 7 ⊢ {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑑)} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}
57	53, 56	eqtri 2764	. . . . . 6 ⊢ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))} = {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}
58	57	mpteq2i 5210	. . . . 5 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)})
59		eleq1w 2820	. . . . . . 7 ⊢ (𝑐 = 𝑦 → (𝑐 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ (𝑓‘𝑥)))
60	59	rabbidv 3415	. . . . . 6 ⊢ (𝑐 = 𝑦 → {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
61	60	cbvmptv 5218	. . . . 5 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑐 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
62	58, 61	eqtri 2764	. . . 4 ⊢ (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (𝑓‘𝑑))}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
63	50, 62	eqtrdi 2792	. . 3 ⊢ (𝑡 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → (𝑐 ∈ 𝐵 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑡𝑑}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
64	20, 21, 35, 63	fmptco 7075	. 2 ⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
65	2, 1	xpexd 7685	. . . . . 6 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
66	65	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → (𝐴 × 𝐵) ∈ V)
67	12	opabbidv 5171	. . . . . . 7 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))})
68		opabssxp 5724	. . . . . . 7 ⊢ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵)
69	67, 68	eqsstrdi 3998	. . . . . 6 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵))
70	69	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ⊆ (𝐴 × 𝐵))
71	66, 70	sselpwd 5283	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) → {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} ∈ 𝒫 (𝐴 × 𝐵))
72		eqid 2736	. . . . 5 ⊢ (𝐴𝑅𝐵) = (𝐴𝑅𝐵)
73	22, 2, 1, 72	rfovcnvd 42267	. . . 4 ⊢ (𝜑 → ◡(𝐴𝑅𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
74		fsovd.cnv	. . . . . 6 ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠))
75	74	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠)))
76		xpeq12 5658	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 × 𝑏) = (𝐴 × 𝐵))
77	76	pweqd 4577	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝐵))
78	77	mpteq1d 5200	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
79	78	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ◡𝑠) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
80	2	elexd 3465	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
81	1	elexd 3465	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
82		pwexg 5333	. . . . . 6 ⊢ ((𝐴 × 𝐵) ∈ V → 𝒫 (𝐴 × 𝐵) ∈ V)
83		mptexg 7171	. . . . . 6 ⊢ (𝒫 (𝐴 × 𝐵) ∈ V → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V)
84	65, 82, 83	3syl 18	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠) ∈ V)
85	75, 79, 80, 81, 84	ovmpod 7507	. . . 4 ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑠 ∈ 𝒫 (𝐴 × 𝐵) ↦ ◡𝑠))
86		cnveq 5829	. . . . 5 ⊢ (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = ◡{⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
87		cnvopab 6091	. . . . 5 ⊢ ◡{⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}
88	86, 87	eqtrdi 2792	. . . 4 ⊢ (𝑠 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))} → ◡𝑠 = {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})
89	71, 73, 85, 88	fmptco 7075	. . 3 ⊢ (𝜑 → ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵)) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))}))
90	89	coeq2d 5818	. 2 ⊢ (𝜑 → ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))) = ((𝐵𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑣, 𝑢⟩ ∣ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))})))
91		fsovd.fs	. . 3 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
92	91, 2, 1	fsovd 42270	. 2 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
93	64, 90, 92	3eqtr4rd 2787	1 ⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ◡(𝐴𝑅𝐵))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3407  Vcvv 3445   ⊆ wss 3910  𝒫 cpw 4560  ⟨cop 4592   class class class wbr 5105  {copab 5167   ↦ cmpt 5188   × cxp 5631  ^◡ccnv 5632   ∘ ccom 5637  ‘cfv 6496  (class class class)co 7357   ∈ cmpo 7359   ↑_m cmap 8765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767

This theorem is referenced by: (None)