Theorem noxpordse

Description: Next we establish the set-like nature of the relationship. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	noxpord.1	|- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) }
	noxpord.2	|- S = { <. x , y >. | ( x e. ( No X. No ) /\ y e. ( No X. No ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) R ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
Assertion	noxpordse	|- S Se ( No X. No )

Proof

Step	Hyp	Ref	Expression
1		noxpord.1	|- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) }
2		noxpord.2	|- S = { <. x , y >. | ( x e. ( No X. No ) /\ y e. ( No X. No ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) R ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
3	1	lrrecse	|- R Se No
4	3	a1i	|- ( T. -> R Se No )
5	2 4 4	sexp2	|- ( T. -> S Se ( No X. No ) )
6	5	mptru	|- S Se ( No X. No )