| Step |
Hyp |
Ref |
Expression |
| 1 |
|
catprs.1 |
|- ( ph -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) ) |
| 2 |
|
catprslem.x |
|- ( ph -> X e. B ) |
| 3 |
|
catprslem.y |
|- ( ph -> Y e. B ) |
| 4 |
|
breq1 |
|- ( x = z -> ( x .<_ y <-> z .<_ y ) ) |
| 5 |
|
oveq1 |
|- ( x = z -> ( x H y ) = ( z H y ) ) |
| 6 |
5
|
neeq1d |
|- ( x = z -> ( ( x H y ) =/= (/) <-> ( z H y ) =/= (/) ) ) |
| 7 |
4 6
|
bibi12d |
|- ( x = z -> ( ( x .<_ y <-> ( x H y ) =/= (/) ) <-> ( z .<_ y <-> ( z H y ) =/= (/) ) ) ) |
| 8 |
|
breq2 |
|- ( y = w -> ( z .<_ y <-> z .<_ w ) ) |
| 9 |
|
oveq2 |
|- ( y = w -> ( z H y ) = ( z H w ) ) |
| 10 |
9
|
neeq1d |
|- ( y = w -> ( ( z H y ) =/= (/) <-> ( z H w ) =/= (/) ) ) |
| 11 |
8 10
|
bibi12d |
|- ( y = w -> ( ( z .<_ y <-> ( z H y ) =/= (/) ) <-> ( z .<_ w <-> ( z H w ) =/= (/) ) ) ) |
| 12 |
7 11
|
cbvral2vw |
|- ( A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) <-> A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) ) |
| 13 |
1 12
|
sylib |
|- ( ph -> A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) ) |
| 14 |
|
breq12 |
|- ( ( z = X /\ w = Y ) -> ( z .<_ w <-> X .<_ Y ) ) |
| 15 |
|
oveq12 |
|- ( ( z = X /\ w = Y ) -> ( z H w ) = ( X H Y ) ) |
| 16 |
15
|
neeq1d |
|- ( ( z = X /\ w = Y ) -> ( ( z H w ) =/= (/) <-> ( X H Y ) =/= (/) ) ) |
| 17 |
14 16
|
bibi12d |
|- ( ( z = X /\ w = Y ) -> ( ( z .<_ w <-> ( z H w ) =/= (/) ) <-> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) ) |
| 18 |
17
|
rspc2gv |
|- ( ( X e. B /\ Y e. B ) -> ( A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) ) |
| 19 |
2 3 18
|
syl2anc |
|- ( ph -> ( A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) ) |
| 20 |
13 19
|
mpd |
|- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) |