ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  inl11 GIF version

Theorem inl11 6953
Description: Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.)
Assertion
Ref Expression
inl11 ((𝐴𝑉𝐵𝑊) → ((inl‘𝐴) = (inl‘𝐵) ↔ 𝐴 = 𝐵))

Proof of Theorem inl11
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 df-inl 6935 . . . 4 inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
2 opeq2 3709 . . . 4 (𝑥 = 𝐴 → ⟨∅, 𝑥⟩ = ⟨∅, 𝐴⟩)
3 elex 2697 . . . . 5 (𝐴𝑉𝐴 ∈ V)
43adantr 274 . . . 4 ((𝐴𝑉𝐵𝑊) → 𝐴 ∈ V)
5 0ex 4058 . . . . 5 ∅ ∈ V
6 simpl 108 . . . . 5 ((𝐴𝑉𝐵𝑊) → 𝐴𝑉)
7 opexg 4153 . . . . 5 ((∅ ∈ V ∧ 𝐴𝑉) → ⟨∅, 𝐴⟩ ∈ V)
85, 6, 7sylancr 410 . . . 4 ((𝐴𝑉𝐵𝑊) → ⟨∅, 𝐴⟩ ∈ V)
91, 2, 4, 8fvmptd3 5517 . . 3 ((𝐴𝑉𝐵𝑊) → (inl‘𝐴) = ⟨∅, 𝐴⟩)
10 opeq2 3709 . . . 4 (𝑥 = 𝐵 → ⟨∅, 𝑥⟩ = ⟨∅, 𝐵⟩)
11 elex 2697 . . . . 5 (𝐵𝑊𝐵 ∈ V)
1211adantl 275 . . . 4 ((𝐴𝑉𝐵𝑊) → 𝐵 ∈ V)
135a1i 9 . . . . 5 ((𝐴𝑉𝐵𝑊) → ∅ ∈ V)
14 opexg 4153 . . . . 5 ((∅ ∈ V ∧ 𝐵𝑊) → ⟨∅, 𝐵⟩ ∈ V)
1513, 14sylancom 416 . . . 4 ((𝐴𝑉𝐵𝑊) → ⟨∅, 𝐵⟩ ∈ V)
161, 10, 12, 15fvmptd3 5517 . . 3 ((𝐴𝑉𝐵𝑊) → (inl‘𝐵) = ⟨∅, 𝐵⟩)
179, 16eqeq12d 2154 . 2 ((𝐴𝑉𝐵𝑊) → ((inl‘𝐴) = (inl‘𝐵) ↔ ⟨∅, 𝐴⟩ = ⟨∅, 𝐵⟩))
18 opthg 4163 . . . . 5 ((∅ ∈ V ∧ 𝐴𝑉) → (⟨∅, 𝐴⟩ = ⟨∅, 𝐵⟩ ↔ (∅ = ∅ ∧ 𝐴 = 𝐵)))
195, 18mpan 420 . . . 4 (𝐴𝑉 → (⟨∅, 𝐴⟩ = ⟨∅, 𝐵⟩ ↔ (∅ = ∅ ∧ 𝐴 = 𝐵)))
20 eqid 2139 . . . . 5 ∅ = ∅
2120biantrur 301 . . . 4 (𝐴 = 𝐵 ↔ (∅ = ∅ ∧ 𝐴 = 𝐵))
2219, 21syl6bbr 197 . . 3 (𝐴𝑉 → (⟨∅, 𝐴⟩ = ⟨∅, 𝐵⟩ ↔ 𝐴 = 𝐵))
2322adantr 274 . 2 ((𝐴𝑉𝐵𝑊) → (⟨∅, 𝐴⟩ = ⟨∅, 𝐵⟩ ↔ 𝐴 = 𝐵))
2417, 23bitrd 187 1 ((𝐴𝑉𝐵𝑊) → ((inl‘𝐴) = (inl‘𝐵) ↔ 𝐴 = 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1331  wcel 1480  Vcvv 2686  c0 3363  cop 3530  cfv 5126  inlcinl 6933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4049  ax-nul 4057  ax-pow 4101  ax-pr 4134
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-br 3933  df-opab 3993  df-mpt 3994  df-id 4218  df-xp 4548  df-rel 4549  df-cnv 4550  df-co 4551  df-dm 4552  df-iota 5091  df-fun 5128  df-fv 5134  df-inl 6935
This theorem is referenced by:  omp1eomlem  6982  difinfsnlem  6987
  Copyright terms: Public domain W3C validator