rfovcnvfvd

Description: Value of the converse of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , evaluated at function G . (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$
	rfovcnvfv.g	$⊢ φ \to G \in ({𝒫 B}^{A})$
Assertion	rfovcnvfvd	$⊢ φ \to F^{-1} (G) = \{⟨x, y⟩ \| (x \in A \land y \in G (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		rfovcnvfv.g	$⊢ φ \to G \in ({𝒫 B}^{A})$
6	1 2 3 4	rfovcnvd	$⊢ φ \to F^{-1} = (g \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in g (x))\})$
7		fveq1	$⊢ g = G \to g (x) = G (x)$
8	7	eleq2d	$⊢ g = G \to (y \in g (x) \leftrightarrow y \in G (x))$
9	8	anbi2d	$⊢ g = G \to ((x \in A \land y \in g (x)) \leftrightarrow (x \in A \land y \in G (x)))$
10	9	opabbidv	$⊢ g = G \to \{⟨x, y⟩ \| (x \in A \land y \in g (x))\} = \{⟨x, y⟩ \| (x \in A \land y \in G (x))\}$
11	10	adantl	$⊢ (φ \land g = G) \to \{⟨x, y⟩ \| (x \in A \land y \in g (x))\} = \{⟨x, y⟩ \| (x \in A \land y \in G (x))\}$
12		simprl	$⊢ (φ \land (x \in A \land y \in G (x))) \to x \in A$
13		elmapi	$⊢ G \in ({𝒫 B}^{A}) \to G : A ⟶ 𝒫 B$
14	13	ffvelrnda	$⊢ (G \in ({𝒫 B}^{A}) \land x \in A) \to G (x) \in 𝒫 B$
15	5 14	sylan	$⊢ (φ \land x \in A) \to G (x) \in 𝒫 B$
16	15	elpwid	$⊢ (φ \land x \in A) \to G (x) \subseteq B$
17	16	sseld	$⊢ (φ \land x \in A) \to (y \in G (x) \to y \in B)$
18	17	impr	$⊢ (φ \land (x \in A \land y \in G (x))) \to y \in B$
19	2 3 12 18	opabex2	$⊢ φ \to \{⟨x, y⟩ \| (x \in A \land y \in G (x))\} \in V$
20	6 11 5 19	fvmptd	$⊢ φ \to F^{-1} (G) = \{⟨x, y⟩ \| (x \in A \land y \in G (x))\}$

Metamath Proof Explorer

Theorem rfovcnvfvd

Proof