djulf1o

Description: The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022)

		Ref	Expression
	Assertion	djulf1o	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V$

Proof

Step	Hyp	Ref	Expression
1		df-inl	$⊢ inl = (x \in V ⟼ ⟨\emptyset, x⟩)$
2		0ex	$⊢ \emptyset \in V$
3	2	snid	$⊢ \emptyset \in \{\emptyset\}$
4		opelxpi	$⊢ (\emptyset \in \{\emptyset\} \land x \in V) \to ⟨\emptyset, x⟩ \in (\{\emptyset\} \times V)$
5	3 4	mpan	$⊢ x \in V \to ⟨\emptyset, x⟩ \in (\{\emptyset\} \times V)$
6	5	adantl	$⊢ (⊤ \land x \in V) \to ⟨\emptyset, x⟩ \in (\{\emptyset\} \times V)$
7		fvexd	$⊢ (⊤ \land y \in (\{\emptyset\} \times V)) \to 2^{nd} (y) \in V$
8		1st2nd2	$⊢ y \in (\{\emptyset\} \times V) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
9		xp1st	$⊢ y \in (\{\emptyset\} \times V) \to 1^{st} (y) \in \{\emptyset\}$
10		elsni	$⊢ 1^{st} (y) \in \{\emptyset\} \to 1^{st} (y) = \emptyset$
11	9 10	syl	$⊢ y \in (\{\emptyset\} \times V) \to 1^{st} (y) = \emptyset$
12	11	opeq1d	$⊢ y \in (\{\emptyset\} \times V) \to ⟨1^{st} (y), 2^{nd} (y)⟩ = ⟨\emptyset, 2^{nd} (y)⟩$
13	8 12	eqtrd	$⊢ y \in (\{\emptyset\} \times V) \to y = ⟨\emptyset, 2^{nd} (y)⟩$
14	13	eqeq2d	$⊢ y \in (\{\emptyset\} \times V) \to (⟨\emptyset, x⟩ = y \leftrightarrow ⟨\emptyset, x⟩ = ⟨\emptyset, 2^{nd} (y)⟩)$
15		eqcom	$⊢ ⟨\emptyset, x⟩ = y \leftrightarrow y = ⟨\emptyset, x⟩$
16		eqid	$⊢ \emptyset = \emptyset$
17		vex	$⊢ x \in V$
18	2 17	opth	$⊢ ⟨\emptyset, x⟩ = ⟨\emptyset, 2^{nd} (y)⟩ \leftrightarrow (\emptyset = \emptyset \land x = 2^{nd} (y))$
19	16 18	mpbiran	$⊢ ⟨\emptyset, x⟩ = ⟨\emptyset, 2^{nd} (y)⟩ \leftrightarrow x = 2^{nd} (y)$
20	14 15 19	3bitr3g	$⊢ y \in (\{\emptyset\} \times V) \to (y = ⟨\emptyset, x⟩ \leftrightarrow x = 2^{nd} (y))$
21	20	bicomd	$⊢ y \in (\{\emptyset\} \times V) \to (x = 2^{nd} (y) \leftrightarrow y = ⟨\emptyset, x⟩)$
22	21	ad2antll	$⊢ (⊤ \land (x \in V \land y \in (\{\emptyset\} \times V))) \to (x = 2^{nd} (y) \leftrightarrow y = ⟨\emptyset, x⟩)$
23	1 6 7 22	f1o2d	$⊢ ⊤ \to inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V$
24	23	mptru	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V$

Metamath Proof Explorer

Theorem djulf1o

Proof