Metamath Proof Explorer

Theorem inlresf

Description: The left injection restricted to the left class of a disjoint union is a function from the left class into the disjoint union. (Contributed by AV, 27-Jun-2022)

		Ref	Expression
	Assertion	inlresf	$⊢ ({inl ↾}_{A}) : A ⟶ (A ⊔︀ B)$

Proof

Step	Hyp	Ref	Expression
1		djulf1o	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V$
2		f1ofun	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V \to Fun inl$
3		ffvresb	$⊢ Fun inl \to (({inl ↾}_{A}) : A ⟶ (A ⊔︀ B) \leftrightarrow \forall x \in A (x \in dom inl \land inl (x) \in (A ⊔︀ B)))$
4	1 2 3	mp2b	$⊢ ({inl ↾}_{A}) : A ⟶ (A ⊔︀ B) \leftrightarrow \forall x \in A (x \in dom inl \land inl (x) \in (A ⊔︀ B))$
5		elex	$⊢ x \in A \to x \in V$
6		opex	$⊢ ⟨\emptyset, x⟩ \in V$
7		df-inl	$⊢ inl = (x \in V ⟼ ⟨\emptyset, x⟩)$
8	6 7	dmmpti	$⊢ dom inl = V$
9	5 8	eleqtrrdi	$⊢ x \in A \to x \in dom inl$
10		djulcl	$⊢ x \in A \to inl (x) \in (A ⊔︀ B)$
11	9 10	jca	$⊢ x \in A \to (x \in dom inl \land inl (x) \in (A ⊔︀ B))$
12	4 11	mprgbir	$⊢ ({inl ↾}_{A}) : A ⟶ (A ⊔︀ B)$