Step |
Hyp |
Ref |
Expression |
1 |
|
simprr |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> C e. A ) |
2 |
|
ssequn1 |
|- ( B C_ C <-> ( B u. C ) = C ) |
3 |
|
eleq1 |
|- ( ( B u. C ) = C -> ( ( B u. C ) e. A <-> C e. A ) ) |
4 |
2 3
|
sylbi |
|- ( B C_ C -> ( ( B u. C ) e. A <-> C e. A ) ) |
5 |
1 4
|
syl5ibrcom |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C -> ( B u. C ) e. A ) ) |
6 |
|
simprl |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> B e. A ) |
7 |
|
ssequn2 |
|- ( C C_ B <-> ( B u. C ) = B ) |
8 |
|
eleq1 |
|- ( ( B u. C ) = B -> ( ( B u. C ) e. A <-> B e. A ) ) |
9 |
7 8
|
sylbi |
|- ( C C_ B -> ( ( B u. C ) e. A <-> B e. A ) ) |
10 |
6 9
|
syl5ibrcom |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( C C_ B -> ( B u. C ) e. A ) ) |
11 |
|
sorpssi |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C \/ C C_ B ) ) |
12 |
5 10 11
|
mpjaod |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B u. C ) e. A ) |