SHARE
TWEET

Untitled

a guest Nov 14th, 2019 152 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Theorem “Identity relation” “Relationship via `Id`”:
  2.     x ⦗ Id ⦘ y  ≡  x = y
  3. Proof:
  4.     x ⦗ Id ⦘ y  ≡  x = y
  5.   ≡⟨ “Infix relationship” ⟩
  6.     ⟨ x, y ⟩ ∈ Id  ≡  x = y
  7.   ≡⟨ “Definition of `Id` via 𝕀” ⟩
  8.     ⟨ x, y ⟩ ∈ 𝕀 𝐔  ≡  x = y
  9.   ≡⟨ “Definition of 𝕀” ⟩
  10.     ⟨ x, y ⟩ ∈ { z ❙ z ∈ 𝐔 • ⟨ z, z ⟩ } ≡  x = y
  11.   ≡⟨ “Set membership” ⟩
  12.     (∃ z ❙ z ∈ 𝐔 • ⟨ x, y ⟩ = ⟨ z , z ⟩ ) ≡  x = y
  13.   ≡⟨ “Pair equality” ⟩
  14.     (∃ z ❙ z ∈ 𝐔 • ( x = z ) ∧ ( y = z ) ) ≡  x = y
  15.   ≡⟨ “Trading for ∃” ⟩
  16.     (∃ z ❙ z ∈ 𝐔 ∧ ( x = z ) • ( y = z ) ) ≡  x = y
  17.   ≡⟨ “Symmetry of ∧” ⟩
  18.     (∃ z ❙ ( x = z ) ∧ z ∈ 𝐔 • ( y = z ) ) ≡  x = y
  19.   ≡⟨ “Trading for ∃” ⟩
  20.     (∃ z ❙ ( x = z ) • z ∈ 𝐔 ∧ ( y = z ) ) ≡  x = y
  21.   ≡⟨ “One-point rule for ∃” ⟩
  22.     (z ∈ 𝐔 ∧ ( y = z ))[ z ≔ x ] ≡ x = y
  23.   ≡⟨ Substitution ⟩
  24.     (x ∈ 𝐔 ∧ ( y = x )) ≡  x = y
  25.   ≡⟨ “Universal set” ⟩
  26.     true ∧ ( y = x ) ≡  x = y
  27.   ≡⟨ “Identity of ∧” ⟩
  28.     ( y = x ) ≡  x = y
  29.   ≡⟨ “Reflexivity of ≡” ⟩
  30.     true
  31.  
  32.    
  33.  
  34. Theorem “Identity of ⨾”: Id ⨾ R = R
  35. Proof:
  36.   Using “Relation extensionality”:
  37.     Subproof for `∀ a • ∀ b • a ⦗ Id ⨾ R ⦘ b ≡ a ⦗ R ⦘ b`:
  38.       For any `a`, `b`:
  39.           a ⦗ Id ⨾ R ⦘ b
  40.         ≡⟨ “Relation composition” ⟩
  41.           ∃ c • a ⦗ Id ⦘ c ∧ c ⦗ R ⦘ b
  42.         ≡⟨ “Identity relation” ⟩
  43.           ∃ c • a = c ∧ c ⦗ R ⦘ b
  44.         ≡⟨ “Trading for ∃” ⟩
  45.           ∃ c ❙ a = c • c ⦗ R ⦘ b
  46.         ≡⟨ “One-point rule for ∃” ⟩
  47.           (c ⦗ R ⦘ b)[c ≔ a]
  48.         ≡⟨ Substitution ⟩
  49.           a ⦗ R ⦘ b
  50.  
  51.  
  52. Theorem “Right-identity of ⨾” “Identity of ⨾”:
  53.     R ⨾ Id = R
  54. Proof:
  55.   Using “Relation extensionality”:
  56.     Subproof for `∀ a • ∀ b • a ⦗ R ⨾ Id ⦘ b ≡ a ⦗ R ⦘ b`:
  57.       For any `a`, `b`:
  58.           a ⦗ R ⨾ Id ⦘ b
  59.         ≡⟨ “Relation composition” ⟩
  60.           ∃ c • a ⦗ R ⦘ c ∧ c ⦗ Id ⦘ b
  61.         ≡⟨ “Identity relation” ⟩
  62.           ∃ c • a ⦗ R ⦘ c ∧ c = b
  63.         ≡⟨ “Trading for ∃” ⟩
  64.           ∃ c ❙ c = b • a ⦗ R ⦘ c
  65.         ≡⟨ “One-point rule for ∃” ⟩
  66.           (a ⦗ R ⦘ c)[c ≔ b]
  67.         ≡⟨ Substitution ⟩
  68.           a ⦗ R ⦘ b
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top