Theorem catprslem

Description: Lemma for catprs . (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	catprs.1	|- ( ph -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) )
	catprslem.x	|- ( ph -> X e. B )
	catprslem.y	|- ( ph -> Y e. B )
Assertion	catprslem	|- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) )

Proof

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 ) =/= (/) ) )