Proof of Theorem ml3le
Step | Hyp | Ref
| Expression |
1 | | lear 161 |
. . . . 5
(b ∩ (c ∪ a)) ≤
(c ∪ a) |
2 | 1 | lelor 166 |
. . . 4
(a ∪ (b ∩ (c ∪
a))) ≤ (a ∪ (c ∪
a)) |
3 | | or12 80 |
. . . . 5
(a ∪ (c ∪ a)) =
(c ∪ (a ∪ a)) |
4 | | oridm 110 |
. . . . . 6
(a ∪ a) = a |
5 | 4 | lor 70 |
. . . . 5
(c ∪ (a ∪ a)) =
(c ∪ a) |
6 | | orcom 73 |
. . . . 5
(c ∪ a) = (a ∪
c) |
7 | 3, 5, 6 | 3tr 65 |
. . . 4
(a ∪ (c ∪ a)) =
(a ∪ c) |
8 | 2, 7 | lbtr 139 |
. . 3
(a ∪ (b ∩ (c ∪
a))) ≤ (a ∪ c) |
9 | | leor 159 |
. . . 4
a ≤ (b ∪ a) |
10 | | leao1 162 |
. . . 4
(b ∩ (c ∪ a)) ≤
(b ∪ a) |
11 | 9, 10 | lel2or 170 |
. . 3
(a ∪ (b ∩ (c ∪
a))) ≤ (b ∪ a) |
12 | 8, 11 | ler2an 173 |
. 2
(a ∪ (b ∩ (c ∪
a))) ≤ ((a ∪ c) ∩
(b ∪ a)) |
13 | 9 | mlduali 1126 |
. 2
((a ∪ c) ∩ (b
∪ a)) = (a ∪ (c ∩
(b ∪ a))) |
14 | 12, 13 | lbtr 139 |
1
(a ∪ (b ∩ (c ∪
a))) ≤ (a ∪ (c ∩
(b ∪ a))) |