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

Proof

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