Theorem lrrecpred

Description: Finally, we calculate the value of the predecessor class over R . (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	lrrec.1	No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
Assertion	lrrecpred	Could not format assertion : No typesetting found for |- ( A e. No -> Pred ( R , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	Could not format R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
2		dfpred3g	$$⊢A\in \mathrm{No}\to Pred\left(R,\mathrm{No},A\right)=\left\{b\in \mathrm{No}|bRA\right\}$$
3	1	lrrecval	Could not format ( ( b e. No /\ A e. No ) -> ( b R A <-> b e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) : No typesetting found for |- ( ( b e. No /\ A e. No ) -> ( b R A <-> b e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) with typecode |-
4	3	ancoms	Could not format ( ( A e. No /\ b e. No ) -> ( b R A <-> b e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) : No typesetting found for |- ( ( A e. No /\ b e. No ) -> ( b R A <-> b e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) with typecode |-
5	4	rabbidva	Could not format ( A e. No -> { b e. No | b R A } = { b e. No | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } ) : No typesetting found for |- ( A e. No -> { b e. No | b R A } = { b e. No | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } ) with typecode |-
6		dfrab2	Could not format { b e. No | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } = ( { b | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } i^i No ) : No typesetting found for |- { b e. No | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } = ( { b | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } i^i No ) with typecode |-
7		abid2	Could not format { b | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } = ( ( _Left ` A ) u. ( _Right ` A ) ) : No typesetting found for |- { b | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } = ( ( _Left ` A ) u. ( _Right ` A ) ) with typecode |-
8	7	ineq1i	Could not format ( { b | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } i^i No ) = ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) : No typesetting found for |- ( { b | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } i^i No ) = ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) with typecode |-
9	6 8	eqtri	Could not format { b e. No | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } = ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) : No typesetting found for |- { b e. No | b e. ( ( _Left ` A ) u. ( _Right ` A ) ) } = ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) with typecode |-
10	5 9	eqtrdi	Could not format ( A e. No -> { b e. No | b R A } = ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) ) : No typesetting found for |- ( A e. No -> { b e. No | b R A } = ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) ) with typecode |-
11		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
12	11	a1i	Could not format ( A e. No -> ( _Left ` A ) C_ No ) : No typesetting found for |- ( A e. No -> ( _Left ` A ) C_ No ) with typecode |-
13		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
14	13	a1i	Could not format ( A e. No -> ( _Right ` A ) C_ No ) : No typesetting found for |- ( A e. No -> ( _Right ` A ) C_ No ) with typecode |-
15	12 14	unssd	Could not format ( A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No ) : No typesetting found for |- ( A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No ) with typecode |-
16		df-ss	Could not format ( ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No <-> ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No <-> ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
17	15 16	sylib	Could not format ( A e. No -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( A e. No -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) i^i No ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
18	2 10 17	3eqtrd	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 |-