| Step |
Hyp |
Ref |
Expression |
| 1 |
|
disjrdx.1 |
|- ( ph -> F : A -1-1-onto-> C ) |
| 2 |
|
disjrdx.2 |
|- ( ( ph /\ y = ( F ` x ) ) -> D = B ) |
| 3 |
|
f1of |
|- ( F : A -1-1-onto-> C -> F : A --> C ) |
| 4 |
1 3
|
syl |
|- ( ph -> F : A --> C ) |
| 5 |
4
|
ffvelcdmda |
|- ( ( ph /\ x e. A ) -> ( F ` x ) e. C ) |
| 6 |
|
f1ofveu |
|- ( ( F : A -1-1-onto-> C /\ y e. C ) -> E! x e. A ( F ` x ) = y ) |
| 7 |
1 6
|
sylan |
|- ( ( ph /\ y e. C ) -> E! x e. A ( F ` x ) = y ) |
| 8 |
|
eqcom |
|- ( ( F ` x ) = y <-> y = ( F ` x ) ) |
| 9 |
8
|
reubii |
|- ( E! x e. A ( F ` x ) = y <-> E! x e. A y = ( F ` x ) ) |
| 10 |
7 9
|
sylib |
|- ( ( ph /\ y e. C ) -> E! x e. A y = ( F ` x ) ) |
| 11 |
2
|
eleq2d |
|- ( ( ph /\ y = ( F ` x ) ) -> ( z e. D <-> z e. B ) ) |
| 12 |
5 10 11
|
rmoxfrd |
|- ( ph -> ( E* y e. C z e. D <-> E* x e. A z e. B ) ) |
| 13 |
12
|
bicomd |
|- ( ph -> ( E* x e. A z e. B <-> E* y e. C z e. D ) ) |
| 14 |
13
|
albidv |
|- ( ph -> ( A. z E* x e. A z e. B <-> A. z E* y e. C z e. D ) ) |
| 15 |
|
df-disj |
|- ( Disj_ x e. A B <-> A. z E* x e. A z e. B ) |
| 16 |
|
df-disj |
|- ( Disj_ y e. C D <-> A. z E* y e. C z e. D ) |
| 17 |
14 15 16
|
3bitr4g |
|- ( ph -> ( Disj_ x e. A B <-> Disj_ y e. C D ) ) |