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	|- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
Assertion	lrrecpred	|- ( A e. No -> Pred ( R , No , A ) = ( ( _L ` A ) u. ( _R ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	|- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
2		dfpred3g	|- ( A e. No -> Pred ( R , No , A ) = { b e. No | b R A } )
3	1	lrrecval	|- ( ( b e. No /\ A e. No ) -> ( b R A <-> b e. ( ( _L ` A ) u. ( _R ` A ) ) ) )
4	3	ancoms	|- ( ( A e. No /\ b e. No ) -> ( b R A <-> b e. ( ( _L ` A ) u. ( _R ` A ) ) ) )
5	4	rabbidva	|- ( A e. No -> { b e. No | b R A } = { b e. No | b e. ( ( _L ` A ) u. ( _R ` A ) ) } )
6		dfrab2	|- { b e. No | b e. ( ( _L ` A ) u. ( _R ` A ) ) } = ( { b | b e. ( ( _L ` A ) u. ( _R ` A ) ) } i^i No )
7		abid2	|- { b | b e. ( ( _L ` A ) u. ( _R ` A ) ) } = ( ( _L ` A ) u. ( _R ` A ) )
8	7	ineq1i	|- ( { b | b e. ( ( _L ` A ) u. ( _R ` A ) ) } i^i No ) = ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No )
9	6 8	eqtri	|- { b e. No | b e. ( ( _L ` A ) u. ( _R ` A ) ) } = ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No )
10	5 9	eqtrdi	|- ( A e. No -> { b e. No | b R A } = ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No ) )
11		leftssno	|- ( _L ` A ) C_ No
12	11	a1i	|- ( A e. No -> ( _L ` A ) C_ No )
13		rightssno	|- ( _R ` A ) C_ No
14	13	a1i	|- ( A e. No -> ( _R ` A ) C_ No )
15	12 14	unssd	|- ( A e. No -> ( ( _L ` A ) u. ( _R ` A ) ) C_ No )
16		df-ss	|- ( ( ( _L ` A ) u. ( _R ` A ) ) C_ No <-> ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No ) = ( ( _L ` A ) u. ( _R ` A ) ) )
17	15 16	sylib	|- ( A e. No -> ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No ) = ( ( _L ` A ) u. ( _R ` A ) ) )
18	2 10 17	3eqtrd	|- ( A e. No -> Pred ( R , No , A ) = ( ( _L ` A ) u. ( _R ` A ) ) )