Step |
Hyp |
Ref |
Expression |
1 |
|
or32 |
|- ( ( ( A C. B \/ B C. A ) \/ A = B ) <-> ( ( A C. B \/ A = B ) \/ B C. A ) ) |
2 |
|
sspss |
|- ( A C_ B <-> ( A C. B \/ A = B ) ) |
3 |
|
sspss |
|- ( B C_ A <-> ( B C. A \/ B = A ) ) |
4 |
|
eqcom |
|- ( B = A <-> A = B ) |
5 |
4
|
orbi2i |
|- ( ( B C. A \/ B = A ) <-> ( B C. A \/ A = B ) ) |
6 |
3 5
|
bitri |
|- ( B C_ A <-> ( B C. A \/ A = B ) ) |
7 |
2 6
|
orbi12i |
|- ( ( A C_ B \/ B C_ A ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ A = B ) ) ) |
8 |
|
orordir |
|- ( ( ( A C. B \/ B C. A ) \/ A = B ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ A = B ) ) ) |
9 |
7 8
|
bitr4i |
|- ( ( A C_ B \/ B C_ A ) <-> ( ( A C. B \/ B C. A ) \/ A = B ) ) |
10 |
|
df-3or |
|- ( ( A C. B \/ A = B \/ B C. A ) <-> ( ( A C. B \/ A = B ) \/ B C. A ) ) |
11 |
1 9 10
|
3bitr4i |
|- ( ( A C_ B \/ B C_ A ) <-> ( A C. B \/ A = B \/ B C. A ) ) |