This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )