Step |
Hyp |
Ref |
Expression |
1 |
|
pssirr |
|- -. x C. x |
2 |
|
psstr |
|- ( ( x C. y /\ y C. z ) -> x C. z ) |
3 |
|
vex |
|- x e. _V |
4 |
3
|
brrpss |
|- ( x [C.] x <-> x C. x ) |
5 |
4
|
notbii |
|- ( -. x [C.] x <-> -. x C. x ) |
6 |
|
vex |
|- y e. _V |
7 |
6
|
brrpss |
|- ( x [C.] y <-> x C. y ) |
8 |
|
vex |
|- z e. _V |
9 |
8
|
brrpss |
|- ( y [C.] z <-> y C. z ) |
10 |
7 9
|
anbi12i |
|- ( ( x [C.] y /\ y [C.] z ) <-> ( x C. y /\ y C. z ) ) |
11 |
8
|
brrpss |
|- ( x [C.] z <-> x C. z ) |
12 |
10 11
|
imbi12i |
|- ( ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) <-> ( ( x C. y /\ y C. z ) -> x C. z ) ) |
13 |
5 12
|
anbi12i |
|- ( ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) <-> ( -. x C. x /\ ( ( x C. y /\ y C. z ) -> x C. z ) ) ) |
14 |
1 2 13
|
mpbir2an |
|- ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) |
15 |
14
|
rgenw |
|- A. z e. A ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) |
16 |
15
|
rgen2w |
|- A. x e. A A. y e. A A. z e. A ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) |
17 |
|
df-po |
|- ( [C.] Po A <-> A. x e. A A. y e. A A. z e. A ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) ) |
18 |
16 17
|
mpbir |
|- [C.] Po A |