Theorem prjsprel

Description: Utility theorem regarding the relation used in PrjSp . (Contributed by Steven Nguyen, 29-Apr-2023)

	Ref	Expression
Hypothesis	prjsprel.1	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
Assertion	prjsprel	|- ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
2		simpll	|- ( ( ( x = X /\ y = Y ) /\ l = m ) -> x = X )
3		simpr	|- ( ( ( x = X /\ y = Y ) /\ l = m ) -> l = m )
4		simplr	|- ( ( ( x = X /\ y = Y ) /\ l = m ) -> y = Y )
5	3 4	oveq12d	|- ( ( ( x = X /\ y = Y ) /\ l = m ) -> ( l .x. y ) = ( m .x. Y ) )
6	2 5	eqeq12d	|- ( ( ( x = X /\ y = Y ) /\ l = m ) -> ( x = ( l .x. y ) <-> X = ( m .x. Y ) ) )
7	6	cbvrexdva	|- ( ( x = X /\ y = Y ) -> ( E. l e. K x = ( l .x. y ) <-> E. m e. K X = ( m .x. Y ) ) )
8	7 1	brab2a	|- ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) )