Theorem fsovrfovd 38303

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	|- O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
fsovd.a	|- ( ph -> A e. V )
fsovd.b	|- ( ph -> B e. W )
fsovd.rf	|- R = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( u e. a |-> { v e. b | u r v } ) ) )
fsovd.cnv	|- C = ( a e. _V , b e. _V |-> ( s e. ~P ( a X. b ) |-> `' s ) )

Assertion

Ref	Expression
fsovrfovd	|- ( ph -> ( A O B ) = ( ( B R A ) o. ( ( A C B ) o. `' ( A R B ) ) ) )

Distinct variable groups:   A, a, b, f, r, u, v   A, s, a, b, f, u, v   x, A, y, a, b, f   B, a, b, f, r, u, v   B, s   y, B   W, a, u   ph, a, b, f, r, u, v

Allowed substitution hints:   ph( x, y, s)   B( x)   C( x, y, v, u, f, s, r, a, b)   R( x, y, v, u, f, s, r, a, b)   O( x, y, v, u, f, s, r, a, b)   V( x, y, v, u, f, s, r, a, b)   W( x, y, v, f, s, r, b)

Proof of Theorem fsovrfovd

Dummy variables c d t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fsovd.b	. . . . . 6 |- ( ph -> B e. W )
2		fsovd.a	. . . . . 6 |- ( ph -> A e. V )
3		xpexg 6960	. . . . . 6 |- ( ( B e. W /\ A e. V ) -> ( B X. A ) e. _V )
4	1, 2, 3	syl2anc 693	. . . . 5 |- ( ph -> ( B X. A ) e. _V )
5	4	adantr 481	. . . 4 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( B X. A ) e. _V )
6		elmapi 7879	. . . . . . . . . . . . . . 15 |- ( f e. ( ~P B ^m A ) -> f : A --> ~P B )
7	6	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( f e. ( ~P B ^m A ) /\ u e. A ) -> ( f ` u ) e. ~P B )
8	7	elpwid 4170	. . . . . . . . . . . . 13 |- ( ( f e. ( ~P B ^m A ) /\ u e. A ) -> ( f ` u ) C_ B )
9	8	sseld 3602	. . . . . . . . . . . 12 |- ( ( f e. ( ~P B ^m A ) /\ u e. A ) -> ( v e. ( f ` u ) -> v e. B ) )
10	9	impancom 456	. . . . . . . . . . 11 |- ( ( f e. ( ~P B ^m A ) /\ v e. ( f ` u ) ) -> ( u e. A -> v e. B ) )
11	10	pm4.71d 666	. . . . . . . . . 10 |- ( ( f e. ( ~P B ^m A ) /\ v e. ( f ` u ) ) -> ( u e. A <-> ( u e. A /\ v e. B ) ) )
12	11	ex 450	. . . . . . . . 9 |- ( f e. ( ~P B ^m A ) -> ( v e. ( f ` u ) -> ( u e. A <-> ( u e. A /\ v e. B ) ) ) )
13	12	pm5.32rd 672	. . . . . . . 8 |- ( f e. ( ~P B ^m A ) -> ( ( u e. A /\ v e. ( f ` u ) ) <-> ( ( u e. A /\ v e. B ) /\ v e. ( f ` u ) ) ) )
14		ancom 466	. . . . . . . . 9 |- ( ( u e. A /\ v e. B ) <-> ( v e. B /\ u e. A ) )
15	14	anbi1i 731	. . . . . . . 8 |- ( ( ( u e. A /\ v e. B ) /\ v e. ( f ` u ) ) <-> ( ( v e. B /\ u e. A ) /\ v e. ( f ` u ) ) )
16	13, 15	syl6bb 276	. . . . . . 7 |- ( f e. ( ~P B ^m A ) -> ( ( u e. A /\ v e. ( f ` u ) ) <-> ( ( v e. B /\ u e. A ) /\ v e. ( f ` u ) ) ) )
17	16	opabbidv 4716	. . . . . 6 |- ( f e. ( ~P B ^m A ) -> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } = { <. v , u >. | ( ( v e. B /\ u e. A ) /\ v e. ( f ` u ) ) } )
18		opabssxp 5193	. . . . . 6 |- { <. v , u >. | ( ( v e. B /\ u e. A ) /\ v e. ( f ` u ) ) } C_ ( B X. A )
19	17, 18	syl6eqss 3655	. . . . 5 |- ( f e. ( ~P B ^m A ) -> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } C_ ( B X. A ) )
20	19	adantl 482	. . . 4 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } C_ ( B X. A ) )
21	5, 20	sselpwd 4807	. . 3 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } e. ~P ( B X. A ) )
22		eqidd 2623	. . 3 |- ( ph -> ( f e. ( ~P B ^m A ) |-> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } ) = ( f e. ( ~P B ^m A ) |-> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } ) )
23		fsovd.rf	. . . . 5 |- R = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( u e. a |-> { v e. b | u r v } ) ) )
24	23, 1, 2	rfovd 38295	. . . 4 |- ( ph -> ( B R A ) = ( r e. ~P ( B X. A ) |-> ( u e. B |-> { v e. A | u r v } ) ) )
25		breq 4655	. . . . . . . 8 |- ( r = t -> ( u r v <-> u t v ) )
26	25	rabbidv 3189	. . . . . . 7 |- ( r = t -> { v e. A | u r v } = { v e. A | u t v } )
27	26	mpteq2dv 4745	. . . . . 6 |- ( r = t -> ( u e. B |-> { v e. A | u r v } ) = ( u e. B |-> { v e. A | u t v } ) )
28		breq1 4656	. . . . . . . . 9 |- ( u = c -> ( u t v <-> c t v ) )
29	28	rabbidv 3189	. . . . . . . 8 |- ( u = c -> { v e. A | u t v } = { v e. A | c t v } )
30		breq2 4657	. . . . . . . . 9 |- ( v = d -> ( c t v <-> c t d ) )
31	30	cbvrabv 3199	. . . . . . . 8 |- { v e. A | c t v } = { d e. A | c t d }
32	29, 31	syl6eq 2672	. . . . . . 7 |- ( u = c -> { v e. A | u t v } = { d e. A | c t d } )
33	32	cbvmptv 4750	. . . . . 6 |- ( u e. B |-> { v e. A | u t v } ) = ( c e. B |-> { d e. A | c t d } )
34	27, 33	syl6eq 2672	. . . . 5 |- ( r = t -> ( u e. B |-> { v e. A | u r v } ) = ( c e. B |-> { d e. A | c t d } ) )
35	34	cbvmptv 4750	. . . 4 |- ( r e. ~P ( B X. A ) |-> ( u e. B |-> { v e. A | u r v } ) ) = ( t e. ~P ( B X. A ) |-> ( c e. B |-> { d e. A | c t d } ) )
36	24, 35	syl6eq 2672	. . 3 |- ( ph -> ( B R A ) = ( t e. ~P ( B X. A ) |-> ( c e. B |-> { d e. A | c t d } ) ) )
37		breq 4655	. . . . . . 7 |- ( t = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } -> ( c t d <-> c { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } d ) )
38		df-br 4654	. . . . . . . 8 |- ( c { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } d <-> <. c , d >. e. { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } )
39		vex 3203	. . . . . . . . 9 |- c e. _V
40		vex 3203	. . . . . . . . 9 |- d e. _V
41		eleq1 2689	. . . . . . . . . 10 |- ( v = c -> ( v e. ( f ` u ) <-> c e. ( f ` u ) ) )
42	41	anbi2d 740	. . . . . . . . 9 |- ( v = c -> ( ( u e. A /\ v e. ( f ` u ) ) <-> ( u e. A /\ c e. ( f ` u ) ) ) )
43		eleq1 2689	. . . . . . . . . 10 |- ( u = d -> ( u e. A <-> d e. A ) )
44		fveq2 6191	. . . . . . . . . . 11 |- ( u = d -> ( f ` u ) = ( f ` d ) )
45	44	eleq2d 2687	. . . . . . . . . 10 |- ( u = d -> ( c e. ( f ` u ) <-> c e. ( f ` d ) ) )
46	43, 45	anbi12d 747	. . . . . . . . 9 |- ( u = d -> ( ( u e. A /\ c e. ( f ` u ) ) <-> ( d e. A /\ c e. ( f ` d ) ) ) )
47	39, 40, 42, 46	opelopab 4997	. . . . . . . 8 |- ( <. c , d >. e. { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } <-> ( d e. A /\ c e. ( f ` d ) ) )
48	38, 47	bitri 264	. . . . . . 7 |- ( c { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } d <-> ( d e. A /\ c e. ( f ` d ) ) )
49	37, 48	syl6bb 276	. . . . . 6 |- ( t = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } -> ( c t d <-> ( d e. A /\ c e. ( f ` d ) ) ) )
50	49	rabbidv 3189	. . . . 5 |- ( t = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } -> { d e. A | c t d } = { d e. A | ( d e. A /\ c e. ( f ` d ) ) } )
51	50	mpteq2dv 4745	. . . 4 |- ( t = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } -> ( c e. B |-> { d e. A | c t d } ) = ( c e. B |-> { d e. A | ( d e. A /\ c e. ( f ` d ) ) } ) )
52		ibar 525	. . . . . . . . 9 |- ( d e. A -> ( c e. ( f ` d ) <-> ( d e. A /\ c e. ( f ` d ) ) ) )
53	52	bicomd 213	. . . . . . . 8 |- ( d e. A -> ( ( d e. A /\ c e. ( f ` d ) ) <-> c e. ( f ` d ) ) )
54	53	rabbiia 3185	. . . . . . 7 |- { d e. A | ( d e. A /\ c e. ( f ` d ) ) } = { d e. A | c e. ( f ` d ) }
55		fveq2 6191	. . . . . . . . 9 |- ( d = x -> ( f ` d ) = ( f ` x ) )
56	55	eleq2d 2687	. . . . . . . 8 |- ( d = x -> ( c e. ( f ` d ) <-> c e. ( f ` x ) ) )
57	56	cbvrabv 3199	. . . . . . 7 |- { d e. A | c e. ( f ` d ) } = { x e. A | c e. ( f ` x ) }
58	54, 57	eqtri 2644	. . . . . 6 |- { d e. A | ( d e. A /\ c e. ( f ` d ) ) } = { x e. A | c e. ( f ` x ) }
59	58	mpteq2i 4741	. . . . 5 |- ( c e. B |-> { d e. A | ( d e. A /\ c e. ( f ` d ) ) } ) = ( c e. B |-> { x e. A | c e. ( f ` x ) } )
60		eleq1 2689	. . . . . . 7 |- ( c = y -> ( c e. ( f ` x ) <-> y e. ( f ` x ) ) )
61	60	rabbidv 3189	. . . . . 6 |- ( c = y -> { x e. A | c e. ( f ` x ) } = { x e. A | y e. ( f ` x ) } )
62	61	cbvmptv 4750	. . . . 5 |- ( c e. B |-> { x e. A | c e. ( f ` x ) } ) = ( y e. B |-> { x e. A | y e. ( f ` x ) } )
63	59, 62	eqtri 2644	. . . 4 |- ( c e. B |-> { d e. A | ( d e. A /\ c e. ( f ` d ) ) } ) = ( y e. B |-> { x e. A | y e. ( f ` x ) } )
64	51, 63	syl6eq 2672	. . 3 |- ( t = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } -> ( c e. B |-> { d e. A | c t d } ) = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) )
65	21, 22, 36, 64	fmptco 6396	. 2 |- ( ph -> ( ( B R A ) o. ( f e. ( ~P B ^m A ) |-> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } ) ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
66		xpexg 6960	. . . . . . 7 |- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
67	2, 1, 66	syl2anc 693	. . . . . 6 |- ( ph -> ( A X. B ) e. _V )
68	67	adantr 481	. . . . 5 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( A X. B ) e. _V )
69	13	opabbidv 4716	. . . . . . 7 |- ( f e. ( ~P B ^m A ) -> { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } = { <. u , v >. | ( ( u e. A /\ v e. B ) /\ v e. ( f ` u ) ) } )
70		opabssxp 5193	. . . . . . 7 |- { <. u , v >. | ( ( u e. A /\ v e. B ) /\ v e. ( f ` u ) ) } C_ ( A X. B )
71	69, 70	syl6eqss 3655	. . . . . 6 |- ( f e. ( ~P B ^m A ) -> { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } C_ ( A X. B ) )
72	71	adantl 482	. . . . 5 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } C_ ( A X. B ) )
73	68, 72	sselpwd 4807	. . . 4 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } e. ~P ( A X. B ) )
74		eqid 2622	. . . . . 6 |- ( A R B ) = ( A R B )
75	23, 2, 1, 74	rfovcnvd 38299	. . . . 5 |- ( ph -> `' ( A R B ) = ( f e. ( ~P B ^m A ) |-> { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } ) )
76	75	idi 2	. . . 4 |- ( ph -> `' ( A R B ) = ( f e. ( ~P B ^m A ) |-> { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } ) )
77		fsovd.cnv	. . . . . 6 |- C = ( a e. _V , b e. _V |-> ( s e. ~P ( a X. b ) |-> `' s ) )
78	77	a1i 11	. . . . 5 |- ( ph -> C = ( a e. _V , b e. _V |-> ( s e. ~P ( a X. b ) |-> `' s ) ) )
79		xpeq12 5134	. . . . . . . 8 |- ( ( a = A /\ b = B ) -> ( a X. b ) = ( A X. B ) )
80	79	pweqd 4163	. . . . . . 7 |- ( ( a = A /\ b = B ) -> ~P ( a X. b ) = ~P ( A X. B ) )
81	80	mpteq1d 4738	. . . . . 6 |- ( ( a = A /\ b = B ) -> ( s e. ~P ( a X. b ) |-> `' s ) = ( s e. ~P ( A X. B ) |-> `' s ) )
82	81	adantl 482	. . . . 5 |- ( ( ph /\ ( a = A /\ b = B ) ) -> ( s e. ~P ( a X. b ) |-> `' s ) = ( s e. ~P ( A X. B ) |-> `' s ) )
83	2	elexd 3214	. . . . 5 |- ( ph -> A e. _V )
84	1	elexd 3214	. . . . 5 |- ( ph -> B e. _V )
85		pwexg 4850	. . . . . 6 |- ( ( A X. B ) e. _V -> ~P ( A X. B ) e. _V )
86		mptexg 6484	. . . . . 6 |- ( ~P ( A X. B ) e. _V -> ( s e. ~P ( A X. B ) |-> `' s ) e. _V )
87	67, 85, 86	3syl 18	. . . . 5 |- ( ph -> ( s e. ~P ( A X. B ) |-> `' s ) e. _V )
88	78, 82, 83, 84, 87	ovmpt2d 6788	. . . 4 |- ( ph -> ( A C B ) = ( s e. ~P ( A X. B ) |-> `' s ) )
89		cnveq 5296	. . . . 5 |- ( s = { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } -> `' s = `' { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } )
90		cnvopab 5533	. . . . 5 |- `' { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) }
91	89, 90	syl6eq 2672	. . . 4 |- ( s = { <. u , v >. | ( u e. A /\ v e. ( f ` u ) ) } -> `' s = { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } )
92	73, 76, 88, 91	fmptco 6396	. . 3 |- ( ph -> ( ( A C B ) o. `' ( A R B ) ) = ( f e. ( ~P B ^m A ) |-> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } ) )
93	92	coeq2d 5284	. 2 |- ( ph -> ( ( B R A ) o. ( ( A C B ) o. `' ( A R B ) ) ) = ( ( B R A ) o. ( f e. ( ~P B ^m A ) |-> { <. v , u >. | ( u e. A /\ v e. ( f ` u ) ) } ) ) )
94		fsovd.fs	. . 3 |- O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
95	94, 2, 1	fsovd 38302	. 2 |- ( ph -> ( A O B ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
96	65, 93, 95	3eqtr4rd 2667	1 |- ( ph -> ( A O B ) = ( ( B R A ) o. ( ( A C B ) o. `' ( A R B ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {crab 2916   _Vcvv 3200   C_ wss 3574   ~Pcpw 4158   <.cop 4183   class class class wbr 4653   {copab 4712   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   o. ccom 5118   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   ^m cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859

This theorem is referenced by: (None)