fsovfd

Description: 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 , gives a function between two sets of functions. (Contributed by RP, 27-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$
Assertion	fsovfd	$⊢ φ \to G : {𝒫 B}^{A} ⟶ {𝒫 A}^{B}$

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	1 2 3	fsovd	$⊢ φ \to A O B = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
6	4 5	eqtrid	$⊢ φ \to G = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
7		ssrab2	$⊢ \{x \in A \| y \in f (x)\} \subseteq A$
8	7	a1i	$⊢ φ \to \{x \in A \| y \in f (x)\} \subseteq A$
9	2 8	sselpwd	$⊢ φ \to \{x \in A \| y \in f (x)\} \in 𝒫 A$
10	9	adantr	$⊢ (φ \land y \in B) \to \{x \in A \| y \in f (x)\} \in 𝒫 A$
11	10	fmpttd	$⊢ φ \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) : B ⟶ 𝒫 A$
12	2	pwexd	$⊢ φ \to 𝒫 A \in V$
13	12 3	elmapd	$⊢ φ \to ((y \in B ⟼ \{x \in A \| y \in f (x)\}) \in ({𝒫 A}^{B}) \leftrightarrow (y \in B ⟼ \{x \in A \| y \in f (x)\}) : B ⟶ 𝒫 A)$
14	11 13	mpbird	$⊢ φ \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) \in ({𝒫 A}^{B})$
15	14	adantr	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) \in ({𝒫 A}^{B})$
16	6 15	fmpt3d	$⊢ φ \to G : {𝒫 B}^{A} ⟶ {𝒫 A}^{B}$

Metamath Proof Explorer

Theorem fsovfd

Proof