Theorem rp-brsslt

Description: Binary relation form of a relation, .< , which has been extended from relation R to subsets of class S . Usually, we will assume R Or S . Definition in Alling, p. 2. Generalization of brsslt . (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023)

	Ref	Expression
Hypothesis	nla0001.defsslt	|- .< = { <. a , b >. | ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) }
Assertion	rp-brsslt	|- ( A .< B <-> ( ( A e. _V /\ B e. _V ) /\ ( A C_ S /\ B C_ S /\ A. x e. A A. y e. B x R y ) ) )

Proof

Step	Hyp	Ref	Expression
1		nla0001.defsslt	|- .< = { <. a , b >. | ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) }
2		sseq1	|- ( a = A -> ( a C_ S <-> A C_ S ) )
3		raleq	|- ( a = A -> ( A. x e. a A. y e. b x R y <-> A. x e. A A. y e. b x R y ) )
4	2 3	3anbi13d	|- ( a = A -> ( ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) <-> ( A C_ S /\ b C_ S /\ A. x e. A A. y e. b x R y ) ) )
5		sseq1	|- ( b = B -> ( b C_ S <-> B C_ S ) )
6		raleq	|- ( b = B -> ( A. y e. b x R y <-> A. y e. B x R y ) )
7	6	ralbidv	|- ( b = B -> ( A. x e. A A. y e. b x R y <-> A. x e. A A. y e. B x R y ) )
8	5 7	3anbi23d	|- ( b = B -> ( ( A C_ S /\ b C_ S /\ A. x e. A A. y e. b x R y ) <-> ( A C_ S /\ B C_ S /\ A. x e. A A. y e. B x R y ) ) )
9	4 8 1	bropabg	|- ( A .< B <-> ( ( A e. _V /\ B e. _V ) /\ ( A C_ S /\ B C_ S /\ A. x e. A A. y e. B x R y ) ) )