Theorem noxpordpred

Description: Next we calculate the predecessor class 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	noxpordpred	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> Pred ( S , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-

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	2	xpord2pred	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to Pred\left(S,\left(\mathrm{No}\times \mathrm{No}\right),⟨A,B⟩\right)=\left(\left(Pred\left(R,\mathrm{No},A\right)\cup \left\{A\right\}\right)\times \left(Pred\left(R,\mathrm{No},B\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}$$
4	1	lrrecpred	Could not format ( A e. No -> Pred ( R , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( A e. No -> Pred ( R , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
5	4	adantr	Could not format ( ( A e. No /\ B e. No ) -> Pred ( R , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> Pred ( R , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
6	5	uneq1d	Could not format ( ( A e. No /\ B e. No ) -> ( Pred ( R , No , A ) u. { A } ) = ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( Pred ( R , No , A ) u. { A } ) = ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
7	1	lrrecpred	Could not format ( B e. No -> Pred ( R , No , B ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( B e. No -> Pred ( R , No , B ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
8	7	adantl	Could not format ( ( A e. No /\ B e. No ) -> Pred ( R , No , B ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> Pred ( R , No , B ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
9	8	uneq1d	Could not format ( ( A e. No /\ B e. No ) -> ( Pred ( R , No , B ) u. { B } ) = ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( Pred ( R , No , B ) u. { B } ) = ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
10	6 9	xpeq12d	Could not format ( ( A e. No /\ B e. No ) -> ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) = ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) = ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) with typecode |-
11	10	difeq1d	Could not format ( ( A e. No /\ B e. No ) -> ( ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) \ { <. A , B >. } ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) \ { <. A , B >. } ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-
12	3 11	eqtrd	Could not format ( ( A e. No /\ B e. No ) -> Pred ( S , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> Pred ( S , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-