List of Syntax, Axioms (ax-) and
Definitions (df-)|
Ref | Expression (see link for any distinct variable requirements)
|
| wb 1 | wff a =
b |
| wle 2 | wff a ≤
b |
| wc 3 | wff a C
b |
| wn 4 | term a⊥ |
| tb 5 | term (a
≡ b) |
| wo 6 | term (a ∪
b) |
| wa 7 | term (a ∩
b) |
| wt 8 | term 1 |
| wf 9 | term 0 |
| wle2 10 | term (a
≤2 b) |
| wi0 11 | term (a
→0 b) |
| wi1 12 | term (a
→1 b) |
| wi2 13 | term (a
→2 b) |
| wi3 14 | term (a
→3 b) |
| wi4 15 | term (a
→4 b) |
| wi5 16 | term (a
→5 b) |
| wid0 17 | term (a
≡0 b) |
| wid1 18 | term (a
≡1 b) |
| wid2 19 | term (a
≡2 b) |
| wid3 20 | term (a
≡3 b) |
| wid4 21 | term (a
≡4 b) |
| wid5 22 | term (a
≡5 b) |
| wb3 23 | term (a
↔3 b) |
| wb1 24 | term (a
↔1 b) |
| wo3 25 | term (a
∪3 b) |
| wan3 26 | term (a
∩3 b) |
| wid3oa 27 | term
(a ≡ c ≡OA b) |
| wid4oa 28 | term
(a ≡ c, d
≡OA b) |
| wcmtr 29 | term C (a, b) |
| ax-a1 30 | a = a⊥
⊥ |
| ax-a2 31 | (a ∪ b) =
(b ∪ a) |
| ax-a3 32 | ((a ∪ b) ∪
c) = (a
∪ (b ∪ c)) |
| ax-a4 33 | (a ∪ (b ∪
b⊥ )) = (b ∪ b⊥ ) |
| ax-a5 34 | (a ∪ (a⊥ ∪ b)⊥ ) = a |
| ax-r1 35 | a = b ⇒ b = a |
| ax-r2 36 | a = b
& b =
c ⇒ a = c |
| ax-r4 37 | a = b ⇒ a⊥ = b⊥ |
| ax-r5 38 | a = b ⇒ (a ∪ c) =
(b ∪ c) |
| df-b 39 | (a ≡ b) =
((a⊥ ∪ b⊥ )⊥ ∪
(a ∪ b)⊥ ) |
| df-a 40 | (a ∩ b) =
(a⊥ ∪ b⊥
)⊥ |
| df-t 41 | 1 = (a ∪ a⊥ ) |
| df-f 42 | 0 =
1⊥ |
| df-i0 43 | (a →0 b) = (a⊥ ∪ b) |
| df-i1 44 | (a →1 b) = (a⊥ ∪ (a ∩ b)) |
| df-i2 45 | (a →2 b) = (b ∪
(a⊥ ∩ b⊥ )) |
| df-i3 46 | (a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) |
| df-i4 47 | (a →4 b) = (((a ∩
b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) |
| df-i5 48 | (a →5 b) = (((a ∩
b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) |
| df-id0 49 | (a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a)) |
| df-id1 50 | (a ≡1 b) = ((a ∪
b⊥ ) ∩ (a⊥ ∪ (a ∩ b))) |
| df-id2 51 | (a ≡2 b) = ((a ∪
b⊥ ) ∩ (b ∪ (a⊥ ∩ b⊥ ))) |
| df-id3 52 | (a ≡3 b) = ((a⊥ ∪ b) ∩ (a
∪ (a⊥ ∩ b⊥ ))) |
| df-id4 53 | (a ≡4 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ (a ∩ b))) |
| df-o3 54 | (a ∪3 b) = (a⊥ →3 (a⊥ →3 b)) |
| df-a3 55 | (a ∩3 b) = (a⊥ ∪3 b⊥
)⊥ |
| df-b3 56 | (a ↔3 b) = ((a
→3 b) ∩ (b →3 a)) |
| df-id3oa 57 | (a ≡ c
≡OA b) = (((a →1 c) ∩ (b
→1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c))) |
| df-id4oa 58 | (a ≡ c,
d ≡OA b) = ((a ≡
d ≡OA b) ∪ ((a
≡ d ≡OA c) ∩ (b
≡ d ≡OA c))) |
| df-le 129 | (a ≤2 b) = ((a ∪
b) ≡ b) |
| df-le1 130 | (a ∪ b) =
b ⇒ a ≤ b |
| df-le2 131 | a ≤ b ⇒ (a ∪ b) =
b |
| df-c1 132 | a = ((a ∩
b) ∪ (a ∩ b⊥ ))
⇒ a C b |
| df-c2 133 | a C b ⇒ a = ((a ∩
b) ∪ (a ∩ b⊥ )) |
| df-cmtr 134 | C (a, b) =
(((a ∩ b) ∪ (a
∩ b⊥ )) ∪
((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) |
| ax-wom 361 | (a⊥ ∪ (a ∩ b)) =
1 ⇒ (b ∪ (a⊥ ∩ b⊥ )) = 1 |
| ax-r3 439 | (c ∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪
(a ∪ b)⊥ )
⇒ a = b |
| ax-oadist 994 | e = (((a ∩
c) ∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d)))) & f = (((a ∩
b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& h ≤
(a →1 d)
& j ≤
f
& k ≤
f
& (h
∩ (b →1 d)) ≤ k ⇒ (h ∩ (j ∪
k)) = ((h ∩ j) ∪
(h ∩ k)) |
| ax-3oa 998 | ((a →1 c) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))) ≤ (b →1 c) |
| ax-oal4 1026 | a ≤ b⊥
& c ≤
d⊥ ⇒ ((a ∪ b) ∩
(c ∪ d)) ≤ (b
∪ (a ∩ (c ∪ ((a
∪ c) ∩ (b ∪ d))))) |
| ax-oa6 1030 | a ≤ b⊥
& c ≤
d⊥ & e ≤ f⊥ ⇒ (((a ∪ b) ∩
(c ∪ d)) ∩ (e
∪ f)) ≤ (b ∪ (a ∩
(c ∪ (((a ∪ c) ∩
(b ∪ d)) ∩ (((a
∪ e) ∩ (b ∪ f))
∪ ((c ∪ e) ∩ (d
∪ f))))))) |
| ax-4oa 1033 | ((a →1 d) ∩ (((a
∩ b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c) ∪
((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d)))))) ≤ (b →1 d) |
| ax-newstateeq 1045 | (((a →1 b) →1 (c →1 b)) ∩ ((a
→1 c) ∩ (b →1 a))) ≤ (c
→1 a) |
| df-id5 1047 | (a ≡5 b) = ((a ∩
b) ∪ (a⊥ ∩ b⊥ )) |
| df-b1 1048 | (a ↔1 b) = ((a
→1 b) ∩ (b →1 a)) |
| ax-wdol 1104 | ((a ≡ b)
∪ (a ≡ b⊥ )) = 1 |
| ax-ml 1122 | ((a ∪ b) ∩
(a ∪ c)) ≤ (a
∪ (b ∩ (a ∪ c))) |
| ax-arg 1153 | ((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2) ⇒ ((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2))) |
