Proof of Theorem oadist2a
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ax-a2 31 |
. . 3
(d ∪ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c)))) = (((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d) |
| 2 | 1 | lan 77 |
. 2
((a →2 b) ∩ (d
∪ ((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) = ((a →2 b) ∩ (((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d)) |
| 3 | | ax-a2 31 |
. . . . . . 7
(((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d) = (d ∪
((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c)))) |
| 4 | | oadist2a.1 |
. . . . . . 7
(d ∪ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c)))) ≤ ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c))) |
| 5 | 3, 4 | bltr 138 |
. . . . . 6
(((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d) ≤ ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c))) |
| 6 | 5 | lelan 167 |
. . . . 5
((a →2 b) ∩ (((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d)) ≤ ((a
→2 b) ∩ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))) |
| 7 | | df-i0 43 |
. . . . . . . 8
((b ∪ c) →0 ((a →2 b) ∩ (a
→2 c))) = ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))) |
| 8 | 7 | lan 77 |
. . . . . . 7
((a →2 b) ∩ ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) |
| 9 | | oath1 1004 |
. . . . . . 7
((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ (a
→2 c)) |
| 10 | 8, 9 | ax-r2 36 |
. . . . . 6
((a →2 b) ∩ ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ (a
→2 c)) |
| 11 | | leo 158 |
. . . . . . 7
((a →2 b) ∩ (a
→2 c)) ≤ (((a →2 b) ∩ (a
→2 c)) ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)) |
| 12 | | df-i2 45 |
. . . . . . . 8
((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))) = (((a →2 b) ∩ (a
→2 c)) ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)) |
| 13 | 12 | ax-r1 35 |
. . . . . . 7
(((a →2 b) ∩ (a
→2 c)) ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥ ))
= ((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))) |
| 14 | 11, 13 | lbtr 139 |
. . . . . 6
((a →2 b) ∩ (a
→2 c)) ≤ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c))) |
| 15 | 10, 14 | bltr 138 |
. . . . 5
((a →2 b) ∩ ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c)))) ≤ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c))) |
| 16 | 6, 15 | letr 137 |
. . . 4
((a →2 b) ∩ (((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d)) ≤ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) |
| 17 | 16 | distlem 188 |
. . 3
((a →2 b) ∩ (((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d)) = (((a
→2 b) ∩ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c)))) ∪ ((a
→2 b) ∩ d)) |
| 18 | | ax-a2 31 |
. . 3
(((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c)))) ∪ ((a →2 b) ∩ d)) =
(((a →2 b) ∩ d)
∪ ((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) |
| 19 | 17, 18 | ax-r2 36 |
. 2
((a →2 b) ∩ (((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))) ∪ d)) = (((a
→2 b) ∩ d) ∪ ((a
→2 b) ∩ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c))))) |
| 20 | 2, 19 | ax-r2 36 |
1
((a →2 b) ∩ (d
∪ ((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) = (((a →2 b) ∩ d)
∪ ((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) |
