Theorem rfovcnvf1od 38298

Description: Properties of the operator, ( A O B ), which maps between relations and functions for relations between base sets, A and B. (Contributed by RP, 27-Apr-2021.)

Hypotheses

Ref	Expression
rfovd.rf	|- O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
rfovd.a	|- ( ph -> A e. V )
rfovd.b	|- ( ph -> B e. W )
rfovcnvf1od.f	|- F = ( A O B )

Assertion

Ref	Expression
rfovcnvf1od	|- ( ph -> ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )

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

Allowed substitution hints:   F( x, y, f, r, a, b)   O( x, y, f, r, a, b)   V( x, y, f, r, a, b)   W( y, f, r, b)

Proof of Theorem rfovcnvf1od

Dummy variables u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) )
2		rfovd.b	. . . . . . . 8 |- ( ph -> B e. W )
3		ssrab2 3687	. . . . . . . . 9 |- { y e. B | x r y } C_ B
4	3	a1i 11	. . . . . . . 8 |- ( ph -> { y e. B | x r y } C_ B )
5	2, 4	sselpwd 4807	. . . . . . 7 |- ( ph -> { y e. B | x r y } e. ~P B )
6	5	adantr 481	. . . . . 6 |- ( ( ph /\ x e. A ) -> { y e. B | x r y } e. ~P B )
7		eqid 2622	. . . . . 6 |- ( x e. A |-> { y e. B | x r y } ) = ( x e. A |-> { y e. B | x r y } )
8	6, 7	fmptd 6385	. . . . 5 |- ( ph -> ( x e. A |-> { y e. B | x r y } ) : A --> ~P B )
9		pwexg 4850	. . . . . . 7 |- ( B e. W -> ~P B e. _V )
10	2, 9	syl 17	. . . . . 6 |- ( ph -> ~P B e. _V )
11		rfovd.a	. . . . . 6 |- ( ph -> A e. V )
12	10, 11	elmapd 7871	. . . . 5 |- ( ph -> ( ( x e. A |-> { y e. B | x r y } ) e. ( ~P B ^m A ) <-> ( x e. A |-> { y e. B | x r y } ) : A --> ~P B ) )
13	8, 12	mpbird 247	. . . 4 |- ( ph -> ( x e. A |-> { y e. B | x r y } ) e. ( ~P B ^m A ) )
14	13	adantr 481	. . 3 |- ( ( ph /\ r e. ~P ( A X. B ) ) -> ( x e. A |-> { y e. B | x r y } ) e. ( ~P B ^m A ) )
15		xpexg 6960	. . . . . 6 |- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
16	11, 2, 15	syl2anc 693	. . . . 5 |- ( ph -> ( A X. B ) e. _V )
17	16	adantr 481	. . . 4 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( A X. B ) e. _V )
18	10, 11	elmapd 7871	. . . . . . . . . . . 12 |- ( ph -> ( f e. ( ~P B ^m A ) <-> f : A --> ~P B ) )
19	18	biimpa 501	. . . . . . . . . . 11 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> f : A --> ~P B )
20	19	ffvelrnda 6359	. . . . . . . . . 10 |- ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ x e. A ) -> ( f ` x ) e. ~P B )
21	20	ex 450	. . . . . . . . 9 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( x e. A -> ( f ` x ) e. ~P B ) )
22		elpwi 4168	. . . . . . . . . 10 |- ( ( f ` x ) e. ~P B -> ( f ` x ) C_ B )
23	22	sseld 3602	. . . . . . . . 9 |- ( ( f ` x ) e. ~P B -> ( y e. ( f ` x ) -> y e. B ) )
24	21, 23	syl6 35	. . . . . . . 8 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( x e. A -> ( y e. ( f ` x ) -> y e. B ) ) )
25	24	imdistand 728	. . . . . . 7 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( ( x e. A /\ y e. ( f ` x ) ) -> ( x e. A /\ y e. B ) ) )
26		a1tru 1500	. . . . . . . 8 |- ( ( x e. A /\ y e. ( f ` x ) ) -> T. )
27	26	a1i 11	. . . . . . 7 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( ( x e. A /\ y e. ( f ` x ) ) -> T. ) )
28	25, 27	jcad 555	. . . . . 6 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( ( x e. A /\ y e. ( f ` x ) ) -> ( ( x e. A /\ y e. B ) /\ T. ) ) )
29	28	ssopab2dv 5004	. . . . 5 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } C_ { <. x , y >. | ( ( x e. A /\ y e. B ) /\ T. ) } )
30		opabssxp 5193	. . . . 5 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ T. ) } C_ ( A X. B )
31	29, 30	syl6ss 3615	. . . 4 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } C_ ( A X. B ) )
32	17, 31	sselpwd 4807	. . 3 |- ( ( ph /\ f e. ( ~P B ^m A ) ) -> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } e. ~P ( A X. B ) )
33		simplrr 801	. . . . . 6 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> f e. ( ~P B ^m A ) )
34		elmapfn 7880	. . . . . 6 |- ( f e. ( ~P B ^m A ) -> f Fn A )
35	33, 34	syl 17	. . . . 5 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> f Fn A )
36	2	ad2antrr 762	. . . . . 6 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> B e. W )
37		rabexg 4812	. . . . . . 7 |- ( B e. W -> { y e. B | x r y } e. _V )
38	37	ralrimivw 2967	. . . . . 6 |- ( B e. W -> A. x e. A { y e. B | x r y } e. _V )
39		nfcv 2764	. . . . . . 7 |- F/_ x A
40	39	fnmptf 6016	. . . . . 6 |- ( A. x e. A { y e. B | x r y } e. _V -> ( x e. A |-> { y e. B | x r y } ) Fn A )
41	36, 38, 40	3syl 18	. . . . 5 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> ( x e. A |-> { y e. B | x r y } ) Fn A )
42		dfin5 3582	. . . . . . 7 |- ( B i^i ( f ` u ) ) = { b e. B | b e. ( f ` u ) }
43		simpllr 799	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) )
44	43	simprd 479	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> f e. ( ~P B ^m A ) )
45		elmapi 7879	. . . . . . . . . . 11 |- ( f e. ( ~P B ^m A ) -> f : A --> ~P B )
46	44, 45	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> f : A --> ~P B )
47		simpr 477	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> u e. A )
48	46, 47	ffvelrnd 6360	. . . . . . . . 9 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( f ` u ) e. ~P B )
49	48	elpwid 4170	. . . . . . . 8 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( f ` u ) C_ B )
50		sseqin2 3817	. . . . . . . 8 |- ( ( f ` u ) C_ B <-> ( B i^i ( f ` u ) ) = ( f ` u ) )
51	49, 50	sylib 208	. . . . . . 7 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( B i^i ( f ` u ) ) = ( f ` u ) )
52		ibar 525	. . . . . . . . 9 |- ( u e. A -> ( b e. ( f ` u ) <-> ( u e. A /\ b e. ( f ` u ) ) ) )
53	52	rabbidv 3189	. . . . . . . 8 |- ( u e. A -> { b e. B | b e. ( f ` u ) } = { b e. B | ( u e. A /\ b e. ( f ` u ) ) } )
54	53	adantl 482	. . . . . . 7 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> { b e. B | b e. ( f ` u ) } = { b e. B | ( u e. A /\ b e. ( f ` u ) ) } )
55	42, 51, 54	3eqtr3a 2680	. . . . . 6 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( f ` u ) = { b e. B | ( u e. A /\ b e. ( f ` u ) ) } )
56		breq2 4657	. . . . . . . . . . 11 |- ( y = b -> ( x r y <-> x r b ) )
57	56	cbvrabv 3199	. . . . . . . . . 10 |- { y e. B | x r y } = { b e. B | x r b }
58		breq1 4656	. . . . . . . . . . . 12 |- ( x = a -> ( x r b <-> a r b ) )
59		df-br 4654	. . . . . . . . . . . 12 |- ( a r b <-> <. a , b >. e. r )
60	58, 59	syl6bb 276	. . . . . . . . . . 11 |- ( x = a -> ( x r b <-> <. a , b >. e. r ) )
61	60	rabbidv 3189	. . . . . . . . . 10 |- ( x = a -> { b e. B | x r b } = { b e. B | <. a , b >. e. r } )
62	57, 61	syl5eq 2668	. . . . . . . . 9 |- ( x = a -> { y e. B | x r y } = { b e. B | <. a , b >. e. r } )
63	62	cbvmptv 4750	. . . . . . . 8 |- ( x e. A |-> { y e. B | x r y } ) = ( a e. A |-> { b e. B | <. a , b >. e. r } )
64	63	a1i 11	. . . . . . 7 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( x e. A |-> { y e. B | x r y } ) = ( a e. A |-> { b e. B | <. a , b >. e. r } ) )
65		simpr 477	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) /\ a = u ) -> a = u )
66	65	opeq1d 4408	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) /\ a = u ) -> <. a , b >. = <. u , b >. )
67		simpllr 799	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) /\ a = u ) -> r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
68	66, 67	eleq12d 2695	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) /\ a = u ) -> ( <. a , b >. e. r <-> <. u , b >. e. { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) )
69		vex 3203	. . . . . . . . . 10 |- u e. _V
70		vex 3203	. . . . . . . . . 10 |- b e. _V
71		simpl 473	. . . . . . . . . . . 12 |- ( ( x = u /\ y = b ) -> x = u )
72	71	eleq1d 2686	. . . . . . . . . . 11 |- ( ( x = u /\ y = b ) -> ( x e. A <-> u e. A ) )
73		simpr 477	. . . . . . . . . . . 12 |- ( ( x = u /\ y = b ) -> y = b )
74	71	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( x = u /\ y = b ) -> ( f ` x ) = ( f ` u ) )
75	73, 74	eleq12d 2695	. . . . . . . . . . 11 |- ( ( x = u /\ y = b ) -> ( y e. ( f ` x ) <-> b e. ( f ` u ) ) )
76	72, 75	anbi12d 747	. . . . . . . . . 10 |- ( ( x = u /\ y = b ) -> ( ( x e. A /\ y e. ( f ` x ) ) <-> ( u e. A /\ b e. ( f ` u ) ) ) )
77	69, 70, 76	opelopaba 4991	. . . . . . . . 9 |- ( <. u , b >. e. { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } <-> ( u e. A /\ b e. ( f ` u ) ) )
78	68, 77	syl6bb 276	. . . . . . . 8 |- ( ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) /\ a = u ) -> ( <. a , b >. e. r <-> ( u e. A /\ b e. ( f ` u ) ) ) )
79	78	rabbidv 3189	. . . . . . 7 |- ( ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) /\ a = u ) -> { b e. B | <. a , b >. e. r } = { b e. B | ( u e. A /\ b e. ( f ` u ) ) } )
80	2	ad3antrrr 766	. . . . . . . 8 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> B e. W )
81		rabexg 4812	. . . . . . . 8 |- ( B e. W -> { b e. B | ( u e. A /\ b e. ( f ` u ) ) } e. _V )
82	80, 81	syl 17	. . . . . . 7 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> { b e. B | ( u e. A /\ b e. ( f ` u ) ) } e. _V )
83	64, 79, 47, 82	fvmptd 6288	. . . . . 6 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( ( x e. A |-> { y e. B | x r y } ) ` u ) = { b e. B | ( u e. A /\ b e. ( f ` u ) ) } )
84	55, 83	eqtr4d 2659	. . . . 5 |- ( ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ u e. A ) -> ( f ` u ) = ( ( x e. A |-> { y e. B | x r y } ) ` u ) )
85	35, 41, 84	eqfnfvd 6314	. . . 4 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> f = ( x e. A |-> { y e. B | x r y } ) )
86		simplrl 800	. . . . . . . 8 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> r e. ~P ( A X. B ) )
87	86	elpwid 4170	. . . . . . 7 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> r C_ ( A X. B ) )
88		xpss 5226	. . . . . . 7 |- ( A X. B ) C_ ( _V X. _V )
89	87, 88	syl6ss 3615	. . . . . 6 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> r C_ ( _V X. _V ) )
90		df-rel 5121	. . . . . 6 |- ( Rel r <-> r C_ ( _V X. _V ) )
91	89, 90	sylibr 224	. . . . 5 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> Rel r )
92		relopab 5247	. . . . . 6 |- Rel { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) }
93	92	a1i 11	. . . . 5 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> Rel { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
94		simpl 473	. . . . . . 7 |- ( ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) -> r e. ~P ( A X. B ) )
95	2, 94	anim12i 590	. . . . . 6 |- ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) -> ( B e. W /\ r e. ~P ( A X. B ) ) )
96	95	anim1i 592	. . . . 5 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) )
97		vex 3203	. . . . . . . 8 |- v e. _V
98		simpl 473	. . . . . . . . . 10 |- ( ( x = u /\ y = v ) -> x = u )
99	98	eleq1d 2686	. . . . . . . . 9 |- ( ( x = u /\ y = v ) -> ( x e. A <-> u e. A ) )
100		simpr 477	. . . . . . . . . 10 |- ( ( x = u /\ y = v ) -> y = v )
101	98	fveq2d 6195	. . . . . . . . . 10 |- ( ( x = u /\ y = v ) -> ( f ` x ) = ( f ` u ) )
102	100, 101	eleq12d 2695	. . . . . . . . 9 |- ( ( x = u /\ y = v ) -> ( y e. ( f ` x ) <-> v e. ( f ` u ) ) )
103	99, 102	anbi12d 747	. . . . . . . 8 |- ( ( x = u /\ y = v ) -> ( ( x e. A /\ y e. ( f ` x ) ) <-> ( u e. A /\ v e. ( f ` u ) ) ) )
104	69, 97, 103	opelopaba 4991	. . . . . . 7 |- ( <. u , v >. e. { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } <-> ( u e. A /\ v e. ( f ` u ) ) )
105		breq2 4657	. . . . . . . . . . . 12 |- ( b = v -> ( u r b <-> u r v ) )
106		df-br 4654	. . . . . . . . . . . 12 |- ( u r v <-> <. u , v >. e. r )
107	105, 106	syl6bb 276	. . . . . . . . . . 11 |- ( b = v -> ( u r b <-> <. u , v >. e. r ) )
108	107	elrab 3363	. . . . . . . . . 10 |- ( v e. { b e. B | u r b } <-> ( v e. B /\ <. u , v >. e. r ) )
109	108	anbi2i 730	. . . . . . . . 9 |- ( ( u e. A /\ v e. { b e. B | u r b } ) <-> ( u e. A /\ ( v e. B /\ <. u , v >. e. r ) ) )
110	109	a1i 11	. . . . . . . 8 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> ( ( u e. A /\ v e. { b e. B | u r b } ) <-> ( u e. A /\ ( v e. B /\ <. u , v >. e. r ) ) ) )
111		simplr 792	. . . . . . . . . . . 12 |- ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) -> f = ( x e. A |-> { y e. B | x r y } ) )
112		breq1 4656	. . . . . . . . . . . . . . 15 |- ( x = a -> ( x r y <-> a r y ) )
113	112	rabbidv 3189	. . . . . . . . . . . . . 14 |- ( x = a -> { y e. B | x r y } = { y e. B | a r y } )
114		breq2 4657	. . . . . . . . . . . . . . 15 |- ( y = b -> ( a r y <-> a r b ) )
115	114	cbvrabv 3199	. . . . . . . . . . . . . 14 |- { y e. B | a r y } = { b e. B | a r b }
116	113, 115	syl6eq 2672	. . . . . . . . . . . . 13 |- ( x = a -> { y e. B | x r y } = { b e. B | a r b } )
117	116	cbvmptv 4750	. . . . . . . . . . . 12 |- ( x e. A |-> { y e. B | x r y } ) = ( a e. A |-> { b e. B | a r b } )
118	111, 117	syl6eq 2672	. . . . . . . . . . 11 |- ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) -> f = ( a e. A |-> { b e. B | a r b } ) )
119		breq1 4656	. . . . . . . . . . . . 13 |- ( a = u -> ( a r b <-> u r b ) )
120	119	rabbidv 3189	. . . . . . . . . . . 12 |- ( a = u -> { b e. B | a r b } = { b e. B | u r b } )
121	120	adantl 482	. . . . . . . . . . 11 |- ( ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) /\ a = u ) -> { b e. B | a r b } = { b e. B | u r b } )
122		simpr 477	. . . . . . . . . . 11 |- ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) -> u e. A )
123		rabexg 4812	. . . . . . . . . . . 12 |- ( B e. W -> { b e. B | u r b } e. _V )
124	123	ad3antrrr 766	. . . . . . . . . . 11 |- ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) -> { b e. B | u r b } e. _V )
125	118, 121, 122, 124	fvmptd 6288	. . . . . . . . . 10 |- ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) -> ( f ` u ) = { b e. B | u r b } )
126	125	eleq2d 2687	. . . . . . . . 9 |- ( ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) /\ u e. A ) -> ( v e. ( f ` u ) <-> v e. { b e. B | u r b } ) )
127	126	pm5.32da 673	. . . . . . . 8 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> ( ( u e. A /\ v e. ( f ` u ) ) <-> ( u e. A /\ v e. { b e. B | u r b } ) ) )
128		simplr 792	. . . . . . . . . 10 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> r e. ~P ( A X. B ) )
129	128	elpwid 4170	. . . . . . . . 9 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> r C_ ( A X. B ) )
130	69, 97	opeldm 5328	. . . . . . . . . . . 12 |- ( <. u , v >. e. r -> u e. dom r )
131		dmss 5323	. . . . . . . . . . . . . 14 |- ( r C_ ( A X. B ) -> dom r C_ dom ( A X. B ) )
132		dmxpss 5565	. . . . . . . . . . . . . 14 |- dom ( A X. B ) C_ A
133	131, 132	syl6ss 3615	. . . . . . . . . . . . 13 |- ( r C_ ( A X. B ) -> dom r C_ A )
134	133	sseld 3602	. . . . . . . . . . . 12 |- ( r C_ ( A X. B ) -> ( u e. dom r -> u e. A ) )
135	130, 134	syl5 34	. . . . . . . . . . 11 |- ( r C_ ( A X. B ) -> ( <. u , v >. e. r -> u e. A ) )
136	135	pm4.71rd 667	. . . . . . . . . 10 |- ( r C_ ( A X. B ) -> ( <. u , v >. e. r <-> ( u e. A /\ <. u , v >. e. r ) ) )
137	69, 97	opelrn 5357	. . . . . . . . . . . . 13 |- ( <. u , v >. e. r -> v e. ran r )
138		rnss 5354	. . . . . . . . . . . . . . 15 |- ( r C_ ( A X. B ) -> ran r C_ ran ( A X. B ) )
139		rnxpss 5566	. . . . . . . . . . . . . . 15 |- ran ( A X. B ) C_ B
140	138, 139	syl6ss 3615	. . . . . . . . . . . . . 14 |- ( r C_ ( A X. B ) -> ran r C_ B )
141	140	sseld 3602	. . . . . . . . . . . . 13 |- ( r C_ ( A X. B ) -> ( v e. ran r -> v e. B ) )
142	137, 141	syl5 34	. . . . . . . . . . . 12 |- ( r C_ ( A X. B ) -> ( <. u , v >. e. r -> v e. B ) )
143	142	pm4.71rd 667	. . . . . . . . . . 11 |- ( r C_ ( A X. B ) -> ( <. u , v >. e. r <-> ( v e. B /\ <. u , v >. e. r ) ) )
144	143	anbi2d 740	. . . . . . . . . 10 |- ( r C_ ( A X. B ) -> ( ( u e. A /\ <. u , v >. e. r ) <-> ( u e. A /\ ( v e. B /\ <. u , v >. e. r ) ) ) )
145	136, 144	bitrd 268	. . . . . . . . 9 |- ( r C_ ( A X. B ) -> ( <. u , v >. e. r <-> ( u e. A /\ ( v e. B /\ <. u , v >. e. r ) ) ) )
146	129, 145	syl 17	. . . . . . . 8 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> ( <. u , v >. e. r <-> ( u e. A /\ ( v e. B /\ <. u , v >. e. r ) ) ) )
147	110, 127, 146	3bitr4d 300	. . . . . . 7 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> ( ( u e. A /\ v e. ( f ` u ) ) <-> <. u , v >. e. r ) )
148	104, 147	syl5rbb 273	. . . . . 6 |- ( ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> ( <. u , v >. e. r <-> <. u , v >. e. { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) )
149	148	eqrelrdv2 5219	. . . . 5 |- ( ( ( Rel r /\ Rel { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) /\ ( ( B e. W /\ r e. ~P ( A X. B ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) ) -> r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
150	91, 93, 96, 149	syl21anc 1325	. . . 4 |- ( ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) /\ f = ( x e. A |-> { y e. B | x r y } ) ) -> r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
151	85, 150	impbida 877	. . 3 |- ( ( ph /\ ( r e. ~P ( A X. B ) /\ f e. ( ~P B ^m A ) ) ) -> ( r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } <-> f = ( x e. A |-> { y e. B | x r y } ) ) )
152	1, 14, 32, 151	f1ocnv2d 6886	. 2 |- ( ph -> ( ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )
153		rfovcnvf1od.f	. . . 4 |- F = ( A O B )
154		rfovd.rf	. . . . 5 |- O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
155	154, 11, 2	rfovd 38295	. . . 4 |- ( ph -> ( A O B ) = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
156	153, 155	syl5eq 2668	. . 3 |- ( ph -> F = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
157		f1oeq1 6127	. . . 4 |- ( F = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) -> ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) <-> ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) ) )
158		cnveq 5296	. . . . 5 |- ( F = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) -> `' F = `' ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
159	158	eqeq1d 2624	. . . 4 |- ( F = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) -> ( `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) <-> `' ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )
160	157, 159	anbi12d 747	. . 3 |- ( F = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) -> ( ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) <-> ( ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) ) )
161	156, 160	syl 17	. 2 |- ( ph -> ( ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) <-> ( ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) ) )
162	152, 161	mpbird 247	1 |- ( ph -> ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   T. wtru 1484   e. wcel 1990   A.wral 2912   {crab 2916   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   <.cop 4183   class class class wbr 4653   {copab 4712   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   Rel wrel 5119   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` 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:  rfovcnvd  38299  rfovf1od  38300