rfovcnvf1od

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)

	Ref	Expression
Hypotheses	rfovd.rf	$⊢ O = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ (x \in a ⟼ \{y \in b \| x r y\})))$
	rfovd.a	$⊢ φ \to A \in V$
	rfovd.b	$⊢ φ \to B \in W$
	rfovcnvf1od.f	$⊢ F = A O B$
Assertion	rfovcnvf1od	$⊢ φ \to (F : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land F^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}))$

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	$⊢ O = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ (x \in a ⟼ \{y \in b \| x r y\})))$
2		rfovd.a	$⊢ φ \to A \in V$
3		rfovd.b	$⊢ φ \to B \in W$
4		rfovcnvf1od.f	$⊢ F = A O B$
5		eqid	$⊢ (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))$
6		ssrab2	$⊢ \{y \in B \| x r y\} \subseteq B$
7	6	a1i	$⊢ φ \to \{y \in B \| x r y\} \subseteq B$
8	3 7	sselpwd	$⊢ φ \to \{y \in B \| x r y\} \in 𝒫 B$
9	8	adantr	$⊢ (φ \land x \in A) \to \{y \in B \| x r y\} \in 𝒫 B$
10	9	fmpttd	$⊢ φ \to (x \in A ⟼ \{y \in B \| x r y\}) : A ⟶ 𝒫 B$
11	3	pwexd	$⊢ φ \to 𝒫 B \in V$
12	11 2	elmapd	$⊢ φ \to ((x \in A ⟼ \{y \in B \| x r y\}) \in ({𝒫 B}^{A}) \leftrightarrow (x \in A ⟼ \{y \in B \| x r y\}) : A ⟶ 𝒫 B)$
13	10 12	mpbird	$⊢ φ \to (x \in A ⟼ \{y \in B \| x r y\}) \in ({𝒫 B}^{A})$
14	13	adantr	$⊢ (φ \land r \in 𝒫 (A \times B)) \to (x \in A ⟼ \{y \in B \| x r y\}) \in ({𝒫 B}^{A})$
15	2 3	xpexd	$⊢ φ \to A \times B \in V$
16	15	adantr	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to A \times B \in V$
17	11 2	elmapd	$⊢ φ \to (f \in ({𝒫 B}^{A}) \leftrightarrow f : A ⟶ 𝒫 B)$
18	17	biimpa	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to f : A ⟶ 𝒫 B$
19	18	ffvelrnda	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land x \in A) \to f (x) \in 𝒫 B$
20	19	ex	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to (x \in A \to f (x) \in 𝒫 B)$
21		elpwi	$⊢ f (x) \in 𝒫 B \to f (x) \subseteq B$
22	21	sseld	$⊢ f (x) \in 𝒫 B \to (y \in f (x) \to y \in B)$
23	20 22	syl6	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to (x \in A \to (y \in f (x) \to y \in B))$
24	23	imdistand	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to ((x \in A \land y \in f (x)) \to (x \in A \land y \in B))$
25		trud	$⊢ (x \in A \land y \in f (x)) \to ⊤$
26	24 25	jca2	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to ((x \in A \land y \in f (x)) \to ((x \in A \land y \in B) \land ⊤))$
27	26	ssopab2dv	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \subseteq \{⟨x, y⟩ \| ((x \in A \land y \in B) \land ⊤)\}$
28		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in A \land y \in B) \land ⊤)\} \subseteq A \times B$
29	27 28	sstrdi	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \subseteq A \times B$
30	16 29	sselpwd	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \in 𝒫 (A \times B)$
31		simplrr	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f \in ({𝒫 B}^{A})$
32		elmapfn	$⊢ f \in ({𝒫 B}^{A}) \to f Fn A$
33	31 32	syl	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f Fn A$
34	3	ad2antrr	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to B \in W$
35		rabexg	$⊢ B \in W \to \{y \in B \| x r y\} \in V$
36	35	ralrimivw	$⊢ B \in W \to \forall x \in A \{y \in B \| x r y\} \in V$
37		nfcv	$⊢ \underline{Ⅎ} x A$
38	37	fnmptf	$⊢ \forall x \in A \{y \in B \| x r y\} \in V \to (x \in A ⟼ \{y \in B \| x r y\}) Fn A$
39	34 36 38	3syl	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to (x \in A ⟼ \{y \in B \| x r y\}) Fn A$
40		dfin5	$⊢ B \cap f (u) = \{b \in B \| b \in f (u)\}$
41		simpllr	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))$
42		elmapi	$⊢ f \in ({𝒫 B}^{A}) \to f : A ⟶ 𝒫 B$
43	41 42	simpl2im	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to f : A ⟶ 𝒫 B$
44		simpr	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to u \in A$
45	43 44	ffvelrnd	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to f (u) \in 𝒫 B$
46	45	elpwid	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to f (u) \subseteq B$
47		sseqin2	$⊢ f (u) \subseteq B \leftrightarrow B \cap f (u) = f (u)$
48	46 47	sylib	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to B \cap f (u) = f (u)$
49		ibar	$⊢ u \in A \to (b \in f (u) \leftrightarrow (u \in A \land b \in f (u)))$
50	49	rabbidv	$⊢ u \in A \to \{b \in B \| b \in f (u)\} = \{b \in B \| (u \in A \land b \in f (u))\}$
51	50	adantl	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to \{b \in B \| b \in f (u)\} = \{b \in B \| (u \in A \land b \in f (u))\}$
52	40 48 51	3eqtr3a	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to f (u) = \{b \in B \| (u \in A \land b \in f (u))\}$
53		breq2	$⊢ y = b \to (x r y \leftrightarrow x r b)$
54	53	cbvrabv	$⊢ \{y \in B \| x r y\} = \{b \in B \| x r b\}$
55		breq1	$⊢ x = a \to (x r b \leftrightarrow a r b)$
56		df-br	$⊢ a r b \leftrightarrow ⟨a, b⟩ \in r$
57	55 56	bitrdi	$⊢ x = a \to (x r b \leftrightarrow ⟨a, b⟩ \in r)$
58	57	rabbidv	$⊢ x = a \to \{b \in B \| x r b\} = \{b \in B \| ⟨a, b⟩ \in r\}$
59	54 58	syl5eq	$⊢ x = a \to \{y \in B \| x r y\} = \{b \in B \| ⟨a, b⟩ \in r\}$
60	59	cbvmptv	$⊢ (x \in A ⟼ \{y \in B \| x r y\}) = (a \in A ⟼ \{b \in B \| ⟨a, b⟩ \in r\})$
61		simpr	$⊢ ((((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \land a = u) \to a = u$
62	61	opeq1d	$⊢ ((((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \land a = u) \to ⟨a, b⟩ = ⟨u, b⟩$
63		simpllr	$⊢ ((((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \land a = u) \to r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
64	62 63	eleq12d	$⊢ ((((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \land a = u) \to (⟨a, b⟩ \in r \leftrightarrow ⟨u, b⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
65		vex	$⊢ u \in V$
66		vex	$⊢ b \in V$
67		simpl	$⊢ (x = u \land y = b) \to x = u$
68	67	eleq1d	$⊢ (x = u \land y = b) \to (x \in A \leftrightarrow u \in A)$
69		simpr	$⊢ (x = u \land y = b) \to y = b$
70	67	fveq2d	$⊢ (x = u \land y = b) \to f (x) = f (u)$
71	69 70	eleq12d	$⊢ (x = u \land y = b) \to (y \in f (x) \leftrightarrow b \in f (u))$
72	68 71	anbi12d	$⊢ (x = u \land y = b) \to ((x \in A \land y \in f (x)) \leftrightarrow (u \in A \land b \in f (u)))$
73	65 66 72	opelopaba	$⊢ ⟨u, b⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \leftrightarrow (u \in A \land b \in f (u))$
74	64 73	bitrdi	$⊢ ((((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \land a = u) \to (⟨a, b⟩ \in r \leftrightarrow (u \in A \land b \in f (u)))$
75	74	rabbidv	$⊢ ((((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \land a = u) \to \{b \in B \| ⟨a, b⟩ \in r\} = \{b \in B \| (u \in A \land b \in f (u))\}$
76	3	ad3antrrr	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to B \in W$
77		rabexg	$⊢ B \in W \to \{b \in B \| (u \in A \land b \in f (u))\} \in V$
78	76 77	syl	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to \{b \in B \| (u \in A \land b \in f (u))\} \in V$
79	60 75 44 78	fvmptd2	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to (x \in A ⟼ \{y \in B \| x r y\}) (u) = \{b \in B \| (u \in A \land b \in f (u))\}$
80	52 79	eqtr4d	$⊢ (((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land u \in A) \to f (u) = (x \in A ⟼ \{y \in B \| x r y\}) (u)$
81	33 39 80	eqfnfvd	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f = (x \in A ⟼ \{y \in B \| x r y\})$
82		simplrl	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \in 𝒫 (A \times B)$
83	82	elpwid	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \subseteq A \times B$
84		xpss	$⊢ A \times B \subseteq V \times V$
85	83 84	sstrdi	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \subseteq V \times V$
86		df-rel	$⊢ Rel r \leftrightarrow r \subseteq V \times V$
87	85 86	sylibr	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to Rel r$
88		relopabv	$⊢ Rel \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
89	88	a1i	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to Rel \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
90		simpl	$⊢ (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A})) \to r \in 𝒫 (A \times B)$
91	3 90	anim12i	$⊢ (φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \to (B \in W \land r \in 𝒫 (A \times B))$
92	91	anim1i	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\}))$
93		vex	$⊢ v \in V$
94		simpl	$⊢ (x = u \land y = v) \to x = u$
95	94	eleq1d	$⊢ (x = u \land y = v) \to (x \in A \leftrightarrow u \in A)$
96		simpr	$⊢ (x = u \land y = v) \to y = v$
97	94	fveq2d	$⊢ (x = u \land y = v) \to f (x) = f (u)$
98	96 97	eleq12d	$⊢ (x = u \land y = v) \to (y \in f (x) \leftrightarrow v \in f (u))$
99	95 98	anbi12d	$⊢ (x = u \land y = v) \to ((x \in A \land y \in f (x)) \leftrightarrow (u \in A \land v \in f (u)))$
100	65 93 99	opelopaba	$⊢ ⟨u, v⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \leftrightarrow (u \in A \land v \in f (u))$
101		breq2	$⊢ b = v \to (u r b \leftrightarrow u r v)$
102		df-br	$⊢ u r v \leftrightarrow ⟨u, v⟩ \in r$
103	101 102	bitrdi	$⊢ b = v \to (u r b \leftrightarrow ⟨u, v⟩ \in r)$
104	103	elrab	$⊢ v \in \{b \in B \| u r b\} \leftrightarrow (v \in B \land ⟨u, v⟩ \in r)$
105	104	anbi2i	$⊢ (u \in A \land v \in \{b \in B \| u r b\}) \leftrightarrow (u \in A \land (v \in B \land ⟨u, v⟩ \in r))$
106	105	a1i	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to ((u \in A \land v \in \{b \in B \| u r b\}) \leftrightarrow (u \in A \land (v \in B \land ⟨u, v⟩ \in r)))$
107		simplr	$⊢ (((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \to f = (x \in A ⟼ \{y \in B \| x r y\})$
108		breq1	$⊢ x = a \to (x r y \leftrightarrow a r y)$
109	108	rabbidv	$⊢ x = a \to \{y \in B \| x r y\} = \{y \in B \| a r y\}$
110		breq2	$⊢ y = b \to (a r y \leftrightarrow a r b)$
111	110	cbvrabv	$⊢ \{y \in B \| a r y\} = \{b \in B \| a r b\}$
112	109 111	eqtrdi	$⊢ x = a \to \{y \in B \| x r y\} = \{b \in B \| a r b\}$
113	112	cbvmptv	$⊢ (x \in A ⟼ \{y \in B \| x r y\}) = (a \in A ⟼ \{b \in B \| a r b\})$
114	107 113	eqtrdi	$⊢ (((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \to f = (a \in A ⟼ \{b \in B \| a r b\})$
115		breq1	$⊢ a = u \to (a r b \leftrightarrow u r b)$
116	115	rabbidv	$⊢ a = u \to \{b \in B \| a r b\} = \{b \in B \| u r b\}$
117	116	adantl	$⊢ ((((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \land a = u) \to \{b \in B \| a r b\} = \{b \in B \| u r b\}$
118		simpr	$⊢ (((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \to u \in A$
119		rabexg	$⊢ B \in W \to \{b \in B \| u r b\} \in V$
120	119	ad3antrrr	$⊢ (((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \to \{b \in B \| u r b\} \in V$
121	114 117 118 120	fvmptd	$⊢ (((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \to f (u) = \{b \in B \| u r b\}$
122	121	eleq2d	$⊢ (((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land u \in A) \to (v \in f (u) \leftrightarrow v \in \{b \in B \| u r b\})$
123	122	pm5.32da	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to ((u \in A \land v \in f (u)) \leftrightarrow (u \in A \land v \in \{b \in B \| u r b\}))$
124		simplr	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \in 𝒫 (A \times B)$
125	124	elpwid	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \subseteq A \times B$
126	65 93	opeldm	$⊢ ⟨u, v⟩ \in r \to u \in dom r$
127		dmss	$⊢ r \subseteq A \times B \to dom r \subseteq dom (A \times B)$
128		dmxpss	$⊢ dom (A \times B) \subseteq A$
129	127 128	sstrdi	$⊢ r \subseteq A \times B \to dom r \subseteq A$
130	129	sseld	$⊢ r \subseteq A \times B \to (u \in dom r \to u \in A)$
131	126 130	syl5	$⊢ r \subseteq A \times B \to (⟨u, v⟩ \in r \to u \in A)$
132	131	pm4.71rd	$⊢ r \subseteq A \times B \to (⟨u, v⟩ \in r \leftrightarrow (u \in A \land ⟨u, v⟩ \in r))$
133	65 93	opelrn	$⊢ ⟨u, v⟩ \in r \to v \in ran r$
134		rnss	$⊢ r \subseteq A \times B \to ran r \subseteq ran (A \times B)$
135		rnxpss	$⊢ ran (A \times B) \subseteq B$
136	134 135	sstrdi	$⊢ r \subseteq A \times B \to ran r \subseteq B$
137	136	sseld	$⊢ r \subseteq A \times B \to (v \in ran r \to v \in B)$
138	133 137	syl5	$⊢ r \subseteq A \times B \to (⟨u, v⟩ \in r \to v \in B)$
139	138	pm4.71rd	$⊢ r \subseteq A \times B \to (⟨u, v⟩ \in r \leftrightarrow (v \in B \land ⟨u, v⟩ \in r))$
140	139	anbi2d	$⊢ r \subseteq A \times B \to ((u \in A \land ⟨u, v⟩ \in r) \leftrightarrow (u \in A \land (v \in B \land ⟨u, v⟩ \in r)))$
141	132 140	bitrd	$⊢ r \subseteq A \times B \to (⟨u, v⟩ \in r \leftrightarrow (u \in A \land (v \in B \land ⟨u, v⟩ \in r)))$
142	125 141	syl	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (⟨u, v⟩ \in r \leftrightarrow (u \in A \land (v \in B \land ⟨u, v⟩ \in r)))$
143	106 123 142	3bitr4d	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to ((u \in A \land v \in f (u)) \leftrightarrow ⟨u, v⟩ \in r)$
144	100 143	bitr2id	$⊢ ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (⟨u, v⟩ \in r \leftrightarrow ⟨u, v⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
145	144	eqrelrdv2	$⊢ ((Rel r \land Rel \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land ((B \in W \land r \in 𝒫 (A \times B)) \land f = (x \in A ⟼ \{y \in B \| x r y\}))) \to r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
146	87 89 92 145	syl21anc	$⊢ ((φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
147	81 146	impbida	$⊢ (φ \land (r \in 𝒫 (A \times B) \land f \in ({𝒫 B}^{A}))) \to (r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \leftrightarrow f = (x \in A ⟼ \{y \in B \| x r y\}))$
148	5 14 30 147	f1ocnv2d	$⊢ φ \to ((r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land {(r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))}^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}))$
149	1 2 3	rfovd	$⊢ φ \to A O B = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))$
150	4 149	syl5eq	$⊢ φ \to F = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))$
151		f1oeq1	$⊢ F = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) \to (F : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \leftrightarrow (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A})$
152		cnveq	$⊢ F = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) \to F^{-1} = {(r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))}^{-1}$
153	152	eqeq1d	$⊢ F = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) \to (F^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \leftrightarrow {(r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))}^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}))$
154	151 153	anbi12d	$⊢ F = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) \to ((F : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land F^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})) \leftrightarrow ((r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land {(r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))}^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})))$
155	150 154	syl	$⊢ φ \to ((F : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land F^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})) \leftrightarrow ((r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land {(r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))}^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})))$
156	148 155	mpbird	$⊢ φ \to (F : 𝒫 (A \times B) \underset{1-1 onto}{⟶} {𝒫 B}^{A} \land F^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}))$

Metamath Proof Explorer

Theorem rfovcnvf1od

Proof