Proof of Theorem oa3-4lem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | dfb 94 |
. . . . . 6
(a ≡ b) = ((a ∩
b) ∪ (a⊥ ∩ b⊥ )) |
| 2 | | ax-a2 31 |
. . . . . . . 8
(a⊥ ∪ (a ∩ c)) =
((a ∩ c) ∪ a⊥ ) |
| 3 | | df-i1 44 |
. . . . . . . 8
(a →1 c) = (a⊥ ∪ (a ∩ c)) |
| 4 | | an1 106 |
. . . . . . . . 9
(a⊥ ∩ 1) =
a⊥ |
| 5 | 4 | lor 70 |
. . . . . . . 8
((a ∩ c) ∪ (a⊥ ∩ 1)) = ((a ∩ c) ∪
a⊥ ) |
| 6 | 2, 3, 5 | 3tr1 63 |
. . . . . . 7
(a →1 c) = ((a ∩
c) ∪ (a⊥ ∩ 1)) |
| 7 | | ax-a2 31 |
. . . . . . . 8
(b⊥ ∪ (b ∩ c)) =
((b ∩ c) ∪ b⊥ ) |
| 8 | | df-i1 44 |
. . . . . . . 8
(b →1 c) = (b⊥ ∪ (b ∩ c)) |
| 9 | | an1 106 |
. . . . . . . . 9
(b⊥ ∩ 1) =
b⊥ |
| 10 | 9 | lor 70 |
. . . . . . . 8
((b ∩ c) ∪ (b⊥ ∩ 1)) = ((b ∩ c) ∪
b⊥ ) |
| 11 | 7, 8, 10 | 3tr1 63 |
. . . . . . 7
(b →1 c) = ((b ∩
c) ∪ (b⊥ ∩ 1)) |
| 12 | 6, 11 | 2an 79 |
. . . . . 6
((a →1 c) ∩ (b
→1 c)) = (((a ∩ c) ∪
(a⊥ ∩ 1)) ∩
((b ∩ c) ∪ (b⊥ ∩ 1))) |
| 13 | 1, 12 | 2or 72 |
. . . . 5
((a ≡ b) ∪ ((a
→1 c) ∩ (b →1 c))) = (((a
∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (((a ∩ c) ∪
(a⊥ ∩ 1)) ∩
((b ∩ c) ∪ (b⊥ ∩ 1)))) |
| 14 | 13 | ax-r1 35 |
. . . 4
(((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (((a ∩ c) ∪
(a⊥ ∩ 1)) ∩
((b ∩ c) ∪ (b⊥ ∩ 1)))) = ((a ≡ b)
∪ ((a →1 c) ∩ (b
→1 c))) |
| 15 | 14 | lan 77 |
. . 3
(b ∩ (((a ∩ b) ∪
(a⊥ ∩ b⊥ )) ∪ (((a ∩ c) ∪
(a⊥ ∩ 1)) ∩
((b ∩ c) ∪ (b⊥ ∩ 1))))) = (b ∩ ((a
≡ b) ∪ ((a →1 c) ∩ (b
→1 c)))) |
| 16 | 15 | lor 70 |
. 2
(a ∪ (b ∩ (((a
∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (((a ∩ c) ∪
(a⊥ ∩ 1)) ∩
((b ∩ c) ∪ (b⊥ ∩ 1)))))) = (a ∪ (b ∩
((a ≡ b) ∪ ((a
→1 c) ∩ (b →1 c))))) |
| 17 | 16 | lan 77 |
1
(a⊥ ∩ (a ∪ (b ∩
(((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (((a ∩ c) ∪
(a⊥ ∩ 1)) ∩
((b ∩ c) ∪ (b⊥ ∩ 1))))))) = (a⊥ ∩ (a ∪ (b ∩
((a ≡ b) ∪ ((a
→1 c) ∩ (b →1 c)))))) |
