Step |
Hyp |
Ref |
Expression |
1 |
|
qsdisj.1 |
|- ( ph -> R Er X ) |
2 |
|
qsdisj.2 |
|- ( ph -> B e. ( A /. R ) ) |
3 |
|
qsdisj.3 |
|- ( ph -> C e. ( A /. R ) ) |
4 |
|
eqid |
|- ( A /. R ) = ( A /. R ) |
5 |
|
eqeq1 |
|- ( [ x ] R = B -> ( [ x ] R = C <-> B = C ) ) |
6 |
|
ineq1 |
|- ( [ x ] R = B -> ( [ x ] R i^i C ) = ( B i^i C ) ) |
7 |
6
|
eqeq1d |
|- ( [ x ] R = B -> ( ( [ x ] R i^i C ) = (/) <-> ( B i^i C ) = (/) ) ) |
8 |
5 7
|
orbi12d |
|- ( [ x ] R = B -> ( ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) <-> ( B = C \/ ( B i^i C ) = (/) ) ) ) |
9 |
|
eqeq2 |
|- ( [ y ] R = C -> ( [ x ] R = [ y ] R <-> [ x ] R = C ) ) |
10 |
|
ineq2 |
|- ( [ y ] R = C -> ( [ x ] R i^i [ y ] R ) = ( [ x ] R i^i C ) ) |
11 |
10
|
eqeq1d |
|- ( [ y ] R = C -> ( ( [ x ] R i^i [ y ] R ) = (/) <-> ( [ x ] R i^i C ) = (/) ) ) |
12 |
9 11
|
orbi12d |
|- ( [ y ] R = C -> ( ( [ x ] R = [ y ] R \/ ( [ x ] R i^i [ y ] R ) = (/) ) <-> ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) ) ) |
13 |
1
|
ad2antrr |
|- ( ( ( ph /\ x e. A ) /\ y e. A ) -> R Er X ) |
14 |
|
erdisj |
|- ( R Er X -> ( [ x ] R = [ y ] R \/ ( [ x ] R i^i [ y ] R ) = (/) ) ) |
15 |
13 14
|
syl |
|- ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( [ x ] R = [ y ] R \/ ( [ x ] R i^i [ y ] R ) = (/) ) ) |
16 |
4 12 15
|
ectocld |
|- ( ( ( ph /\ x e. A ) /\ C e. ( A /. R ) ) -> ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) ) |
17 |
3 16
|
mpidan |
|- ( ( ph /\ x e. A ) -> ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) ) |
18 |
4 8 17
|
ectocld |
|- ( ( ph /\ B e. ( A /. R ) ) -> ( B = C \/ ( B i^i C ) = (/) ) ) |
19 |
2 18
|
mpdan |
|- ( ph -> ( B = C \/ ( B i^i C ) = (/) ) ) |