Theorem noxpordfr

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

	Ref	Expression
Hypotheses	noxpord.1	$$⊢R=\left\{⟨a,b⟩|a\in \left(L\left(b\right)\cup R\left(b\right)\right)\right\}$$
	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	noxpordfr	$$⊢S\mathrm{Fr}\left(\mathrm{No}\times \mathrm{No}\right)$$

Proof

Step	Hyp	Ref	Expression
1		noxpord.1	$$⊢R=\left\{⟨a,b⟩|a\in \left(L\left(b\right)\cup R\left(b\right)\right)\right\}$$
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	lrrecfr	$$⊢R\mathrm{Fr}\mathrm{No}$$
4	3	a1i	$$⊢\top \to R\mathrm{Fr}\mathrm{No}$$
5	2 4 4	frxp2	$$⊢\top \to S\mathrm{Fr}\left(\mathrm{No}\times \mathrm{No}\right)$$
6	5	mptru	$$⊢S\mathrm{Fr}\left(\mathrm{No}\times \mathrm{No}\right)$$