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	No typesetting found for |- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } with typecode |-
	noxpord.2	$$⊢S=\left\{⟨x,y⟩|\left(x\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge y\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)R{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}$$
Assertion	noxpordse	$$⊢S\mathrm{Se}\left(\mathrm{No}\times \mathrm{No}\right)$$

Proof

Step	Hyp	Ref	Expression
1		noxpord.1	Could not format R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } : No typesetting found for |- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } with typecode |-
2		noxpord.2	$$⊢S=\left\{⟨x,y⟩|\left(x\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge y\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)R{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}$$
3	1	lrrecse	$$⊢R\mathrm{Se}\mathrm{No}$$
4	3	a1i	$$⊢\top \to R\mathrm{Se}\mathrm{No}$$
5	2 4 4	sexp2	$$⊢\top \to S\mathrm{Se}\left(\mathrm{No}\times \mathrm{No}\right)$$
6	5	mptru	$$⊢S\mathrm{Se}\left(\mathrm{No}\times \mathrm{No}\right)$$