elpmi

Description: A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015)

		Ref	Expression
	Assertion	elpmi	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (F : dom F ⟶ A \land dom F \subseteq B)$

Step	Hyp	Ref	Expression
1		n0i	$⊢ F \in (A ↑_{𝑝𝑚} B) \to \neg A ↑_{𝑝𝑚} B = \emptyset$
2		fnpm	$⊢ ↑_{𝑝𝑚} Fn (V \times V)$
3		fndm	$⊢ ↑_{𝑝𝑚} Fn (V \times V) \to dom ↑_{𝑝𝑚} = V \times V$
4	2 3	ax-mp	$⊢ dom ↑_{𝑝𝑚} = V \times V$
5	4	ndmov	$⊢ \neg (A \in V \land B \in V) \to A ↑_{𝑝𝑚} B = \emptyset$
6	1 5	nsyl2	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (A \in V \land B \in V)$
7		elpm2g	$⊢ (A \in V \land B \in V) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$
8	6 7	syl	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$
9	8	ibi	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (F : dom F ⟶ A \land dom F \subseteq B)$

Metamath Proof Explorer