Step |
Hyp |
Ref |
Expression |
1 |
|
porpss |
|- [C.] Po A |
2 |
1
|
biantrur |
|- ( A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) <-> ( [C.] Po A /\ A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) ) ) |
3 |
|
sspsstri |
|- ( ( x C_ y \/ y C_ x ) <-> ( x C. y \/ x = y \/ y C. x ) ) |
4 |
|
vex |
|- y e. _V |
5 |
4
|
brrpss |
|- ( x [C.] y <-> x C. y ) |
6 |
|
biid |
|- ( x = y <-> x = y ) |
7 |
|
vex |
|- x e. _V |
8 |
7
|
brrpss |
|- ( y [C.] x <-> y C. x ) |
9 |
5 6 8
|
3orbi123i |
|- ( ( x [C.] y \/ x = y \/ y [C.] x ) <-> ( x C. y \/ x = y \/ y C. x ) ) |
10 |
3 9
|
bitr4i |
|- ( ( x C_ y \/ y C_ x ) <-> ( x [C.] y \/ x = y \/ y [C.] x ) ) |
11 |
10
|
2ralbii |
|- ( A. x e. A A. y e. A ( x C_ y \/ y C_ x ) <-> A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) ) |
12 |
|
df-so |
|- ( [C.] Or A <-> ( [C.] Po A /\ A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) ) ) |
13 |
2 11 12
|
3bitr4ri |
|- ( [C.] Or A <-> A. x e. A A. y e. A ( x C_ y \/ y C_ x ) ) |