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	2	fndmi	$⊢ dom ↑_{𝑝𝑚} = V \times V$
4	3	ndmov	$⊢ \neg (A \in V \land B \in V) \to A ↑_{𝑝𝑚} B = \emptyset$
5	1 4	nsyl2	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (A \in V \land B \in V)$
6		elpm2g	$⊢ (A \in V \land B \in V) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$
7	5 6	syl	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$
8	7	ibi	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (F : dom F ⟶ A \land dom F \subseteq B)$

Metamath Proof Explorer