Theorem djurf1o

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

	Ref	Expression
Assertion	djurf1o	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-inr	$$⊢inr=\left(x\in \mathrm{V}⟼⟨1_{𝑜},x⟩\right)$$
2		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
3		snidg	$$⊢1_{𝑜}\in \mathrm{\omega }\to 1_{𝑜}\in \left\{1_{𝑜}\right\}$$
4	2 3	ax-mp	$$⊢1_{𝑜}\in \left\{1_{𝑜}\right\}$$
5		opelxpi	$$⊢\left(1_{𝑜}\in \left\{1_{𝑜}\right\}\wedge x\in \mathrm{V}\right)\to ⟨1_{𝑜},x⟩\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)$$
6	4 5	mpan	$$⊢x\in \mathrm{V}\to ⟨1_{𝑜},x⟩\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)$$
7	6	adantl	$$⊢\left(\top \wedge x\in \mathrm{V}\right)\to ⟨1_{𝑜},x⟩\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)$$
8		fvexd	$$⊢\left(\top \wedge y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\right)\to 2^{nd}\left(y\right)\in \mathrm{V}$$
9		1st2nd2	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
10		xp1st	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to 1^{st}\left(y\right)\in \left\{1_{𝑜}\right\}$$
11		elsni	$$⊢1^{st}\left(y\right)\in \left\{1_{𝑜}\right\}\to 1^{st}\left(y\right)=1_{𝑜}$$
12	10 11	syl	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to 1^{st}\left(y\right)=1_{𝑜}$$
13	12	opeq1d	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to ⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩=⟨1_{𝑜},2^{nd}\left(y\right)⟩$$
14	9 13	eqtrd	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to y=⟨1_{𝑜},2^{nd}\left(y\right)⟩$$
15	14	eqeq2d	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to \left(⟨1_{𝑜},x⟩=y\leftrightarrow ⟨1_{𝑜},x⟩=⟨1_{𝑜},2^{nd}\left(y\right)⟩\right)$$
16		eqcom	$$⊢⟨1_{𝑜},x⟩=y\leftrightarrow y=⟨1_{𝑜},x⟩$$
17		eqid	$$⊢1_{𝑜}=1_{𝑜}$$
18		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
19		vex	$$⊢x\in \mathrm{V}$$
20	18 19	opth	$$⊢⟨1_{𝑜},x⟩=⟨1_{𝑜},2^{nd}\left(y\right)⟩\leftrightarrow \left(1_{𝑜}=1_{𝑜}\wedge x=2^{nd}\left(y\right)\right)$$
21	17 20	mpbiran	$$⊢⟨1_{𝑜},x⟩=⟨1_{𝑜},2^{nd}\left(y\right)⟩\leftrightarrow x=2^{nd}\left(y\right)$$
22	15 16 21	3bitr3g	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to \left(y=⟨1_{𝑜},x⟩\leftrightarrow x=2^{nd}\left(y\right)\right)$$
23	22	bicomd	$$⊢y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\to \left(x=2^{nd}\left(y\right)\leftrightarrow y=⟨1_{𝑜},x⟩\right)$$
24	23	ad2antll	$$⊢\left(\top \wedge \left(x\in \mathrm{V}\wedge y\in \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\right)\right)\to \left(x=2^{nd}\left(y\right)\leftrightarrow y=⟨1_{𝑜},x⟩\right)$$
25	1 7 8 24	f1o2d	$$⊢\top \to inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$
26	25	mptru	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$