Step |
Hyp |
Ref |
Expression |
1 |
|
djuen |
|- ( ( A ~~ B /\ C ~~ D ) -> ( A |_| C ) ~~ ( B |_| D ) ) |
2 |
1
|
3adant3 |
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A |_| C ) ~~ ( B |_| D ) ) |
3 |
|
relen |
|- Rel ~~ |
4 |
3
|
brrelex2i |
|- ( A ~~ B -> B e. _V ) |
5 |
3
|
brrelex2i |
|- ( C ~~ D -> D e. _V ) |
6 |
|
id |
|- ( ( B i^i D ) = (/) -> ( B i^i D ) = (/) ) |
7 |
|
endjudisj |
|- ( ( B e. _V /\ D e. _V /\ ( B i^i D ) = (/) ) -> ( B |_| D ) ~~ ( B u. D ) ) |
8 |
4 5 6 7
|
syl3an |
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( B |_| D ) ~~ ( B u. D ) ) |
9 |
|
entr |
|- ( ( ( A |_| C ) ~~ ( B |_| D ) /\ ( B |_| D ) ~~ ( B u. D ) ) -> ( A |_| C ) ~~ ( B u. D ) ) |
10 |
2 8 9
|
syl2anc |
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A |_| C ) ~~ ( B u. D ) ) |