inj_intro

Theorem inj_intro

Theorem. inj_intro
map f X Y → (∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b) → inj f X Y

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ ∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b, hypo.
03. 1, 2 ⊢ map f X Y ∧
  ∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b, conj_intro 1 2.
04. 1, 2 ⊢ inj f X Y, rsubj_elim inj_equi 3.
inj_intro. ⊢ map f X Y →
  (∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b) →
  inj f X Y, subj_intro_ii 4.