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 : V –1-1-onto→ ( { 1_o } × V )

Proof

Step	Hyp	Ref	Expression
1		df-inr	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1_o , 𝑥 ⟩ )
2		1onn	⊢ 1_o ∈ ω
3		snidg	⊢ ( 1_o ∈ ω → 1_o ∈ { 1_o } )
4	2 3	ax-mp	⊢ 1_o ∈ { 1_o }
5		opelxpi	⊢ ( ( 1_o ∈ { 1_o } ∧ 𝑥 ∈ V ) → ⟨ 1_o , 𝑥 ⟩ ∈ ( { 1_o } × V ) )
6	4 5	mpan	⊢ ( 𝑥 ∈ V → ⟨ 1_o , 𝑥 ⟩ ∈ ( { 1_o } × V ) )
7	6	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ V ) → ⟨ 1_o , 𝑥 ⟩ ∈ ( { 1_o } × V ) )
8		fvexd	⊢ ( ( ⊤ ∧ 𝑦 ∈ ( { 1_o } × V ) ) → ( 2^nd ‘ 𝑦 ) ∈ V )
9		1st2nd2	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
10		xp1st	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → ( 1^st ‘ 𝑦 ) ∈ { 1_o } )
11		elsni	⊢ ( ( 1^st ‘ 𝑦 ) ∈ { 1_o } → ( 1^st ‘ 𝑦 ) = 1_o )
12	10 11	syl	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → ( 1^st ‘ 𝑦 ) = 1_o )
13	12	opeq1d	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ = ⟨ 1_o , ( 2^nd ‘ 𝑦 ) ⟩ )
14	9 13	eqtrd	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → 𝑦 = ⟨ 1_o , ( 2^nd ‘ 𝑦 ) ⟩ )
15	14	eqeq2d	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → ( ⟨ 1_o , 𝑥 ⟩ = 𝑦 ↔ ⟨ 1_o , 𝑥 ⟩ = ⟨ 1_o , ( 2^nd ‘ 𝑦 ) ⟩ ) )
16		eqcom	⊢ ( ⟨ 1_o , 𝑥 ⟩ = 𝑦 ↔ 𝑦 = ⟨ 1_o , 𝑥 ⟩ )
17		eqid	⊢ 1_o = 1_o
18		1oex	⊢ 1_o ∈ V
19		vex	⊢ 𝑥 ∈ V
20	18 19	opth	⊢ ( ⟨ 1_o , 𝑥 ⟩ = ⟨ 1_o , ( 2^nd ‘ 𝑦 ) ⟩ ↔ ( 1_o = 1_o ∧ 𝑥 = ( 2^nd ‘ 𝑦 ) ) )
21	17 20	mpbiran	⊢ ( ⟨ 1_o , 𝑥 ⟩ = ⟨ 1_o , ( 2^nd ‘ 𝑦 ) ⟩ ↔ 𝑥 = ( 2^nd ‘ 𝑦 ) )
22	15 16 21	3bitr3g	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → ( 𝑦 = ⟨ 1_o , 𝑥 ⟩ ↔ 𝑥 = ( 2^nd ‘ 𝑦 ) ) )
23	22	bicomd	⊢ ( 𝑦 ∈ ( { 1_o } × V ) → ( 𝑥 = ( 2^nd ‘ 𝑦 ) ↔ 𝑦 = ⟨ 1_o , 𝑥 ⟩ ) )
24	23	ad2antll	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( { 1_o } × V ) ) ) → ( 𝑥 = ( 2^nd ‘ 𝑦 ) ↔ 𝑦 = ⟨ 1_o , 𝑥 ⟩ ) )
25	1 7 8 24	f1o2d	⊢ ( ⊤ → inr : V –1-1-onto→ ( { 1_o } × V ) )
26	25	mptru	⊢ inr : V –1-1-onto→ ( { 1_o } × V )

Metamath Proof Explorer

Theorem djurf1o

Proof