Step |
Hyp |
Ref |
Expression |
1 |
|
df-co |
|- ( A o. B ) = { <. x , z >. | E. y ( x B y /\ y A z ) } |
2 |
1
|
relopabiv |
|- Rel ( A o. B ) |
3 |
|
ssrel |
|- ( Rel ( A o. B ) -> ( ( A o. B ) C_ C <-> A. x A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) ) ) |
4 |
2 3
|
ax-mp |
|- ( ( A o. B ) C_ C <-> A. x A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) ) |
5 |
|
vex |
|- x e. _V |
6 |
|
vex |
|- z e. _V |
7 |
5 6
|
opelco |
|- ( <. x , z >. e. ( A o. B ) <-> E. y ( x B y /\ y A z ) ) |
8 |
|
df-br |
|- ( x C z <-> <. x , z >. e. C ) |
9 |
8
|
bicomi |
|- ( <. x , z >. e. C <-> x C z ) |
10 |
7 9
|
imbi12i |
|- ( ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> ( E. y ( x B y /\ y A z ) -> x C z ) ) |
11 |
|
19.23v |
|- ( A. y ( ( x B y /\ y A z ) -> x C z ) <-> ( E. y ( x B y /\ y A z ) -> x C z ) ) |
12 |
10 11
|
bitr4i |
|- ( ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. y ( ( x B y /\ y A z ) -> x C z ) ) |
13 |
12
|
albii |
|- ( A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. z A. y ( ( x B y /\ y A z ) -> x C z ) ) |
14 |
|
alcom |
|- ( A. z A. y ( ( x B y /\ y A z ) -> x C z ) <-> A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) |
15 |
13 14
|
bitri |
|- ( A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) |
16 |
15
|
albii |
|- ( A. x A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) |
17 |
4 16
|
bitri |
|- ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) |