• API
• FAQ
• Tools
• Archive
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.
Not a member of Pastebin yet?