Theorem noxpordfr

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

	Ref	Expression
Hypotheses	noxpord.1	|- R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` 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	noxpordfr	|- S Fr ( No X. No )

Proof

Step	Hyp	Ref	Expression
1		noxpord.1	|- R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` 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	lrrecfr	|- R Fr No
4	3	a1i	|- ( T. -> R Fr No )
5	2 4 4	frxp2	|- ( T. -> S Fr ( No X. No ) )
6	5	mptru	|- S Fr ( No X. No )