fsovfvd

Description: Value of the operator, ( A O B ) , which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, A and B , when applied to function F . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	fsovd.fs	$⊢ O = (a \in V, b \in V ⟼ (f \in ({𝒫 b}^{a}) ⟼ (y \in b ⟼ \{x \in a \| y \in f (x)\})))$
	fsovd.a	$⊢ φ \to A \in V$
	fsovd.b	$⊢ φ \to B \in W$
	fsovfvd.g	$⊢ G = A O B$
	fsovfvd.f	$⊢ φ \to F \in ({𝒫 B}^{A})$
Assertion	fsovfvd	$⊢ φ \to G (F) = (y \in B ⟼ \{x \in A \| y \in F (x)\})$

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	$⊢ O = (a \in V, b \in V ⟼ (f \in ({𝒫 b}^{a}) ⟼ (y \in b ⟼ \{x \in a \| y \in f (x)\})))$
2		fsovd.a	$⊢ φ \to A \in V$
3		fsovd.b	$⊢ φ \to B \in W$
4		fsovfvd.g	$⊢ G = A O B$
5		fsovfvd.f	$⊢ φ \to F \in ({𝒫 B}^{A})$
6	1 2 3	fsovd	$⊢ φ \to A O B = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
7	4 6	syl5eq	$⊢ φ \to G = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
8		fveq1	$⊢ f = F \to f (x) = F (x)$
9	8	eleq2d	$⊢ f = F \to (y \in f (x) \leftrightarrow y \in F (x))$
10	9	rabbidv	$⊢ f = F \to \{x \in A \| y \in f (x)\} = \{x \in A \| y \in F (x)\}$
11	10	mpteq2dv	$⊢ f = F \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) = (y \in B ⟼ \{x \in A \| y \in F (x)\})$
12	11	adantl	$⊢ (φ \land f = F) \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) = (y \in B ⟼ \{x \in A \| y \in F (x)\})$
13	3	mptexd	$⊢ φ \to (y \in B ⟼ \{x \in A \| y \in F (x)\}) \in V$
14	7 12 5 13	fvmptd	$⊢ φ \to G (F) = (y \in B ⟼ \{x \in A \| y \in F (x)\})$

Metamath Proof Explorer

Theorem fsovfvd

Proof