Metamath Proof Explorer

Theorem rfovd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B . (Contributed by RP, 25-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$
	Assertion	rfovd	$⊢ φ \to A O B = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))$

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	1	a1i	$⊢ φ \to O = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ (x \in a ⟼ \{y \in b \| x r y\})))$
5		xpeq12	$⊢ (a = A \land b = B) \to a \times b = A \times B$
6	5	pweqd	$⊢ (a = A \land b = B) \to 𝒫 (a \times b) = 𝒫 (A \times B)$
7		simpl	$⊢ (a = A \land b = B) \to a = A$
8		rabeq	$⊢ b = B \to \{y \in b \| x r y\} = \{y \in B \| x r y\}$
9	8	adantl	$⊢ (a = A \land b = B) \to \{y \in b \| x r y\} = \{y \in B \| x r y\}$
10	7 9	mpteq12dv	$⊢ (a = A \land b = B) \to (x \in a ⟼ \{y \in b \| x r y\}) = (x \in A ⟼ \{y \in B \| x r y\})$
11	6 10	mpteq12dv	$⊢ (a = A \land b = B) \to (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\}))$
12	11	adantl	$⊢ (φ \land (a = A \land b = B)) \to (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\}))$
13	2	elexd	$⊢ φ \to A \in V$
14	3	elexd	$⊢ φ \to B \in V$
15	2 3	xpexd	$⊢ φ \to A \times B \in V$
16		pwexg	$⊢ A \times B \in V \to 𝒫 (A \times B) \in V$
17		mptexg	$⊢ 𝒫 (A \times B) \in V \to (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) \in V$
18	15 16 17	3syl	$⊢ φ \to (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\})) \in V$
19	4 12 13 14 18	ovmpod	$⊢ φ \to A O B = (r \in 𝒫 (A \times B) ⟼ (x \in A ⟼ \{y \in B \| x r y\}))$