Theorem lrrecse

Description: Next, we show that R is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	lrrec.1	|- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
Assertion	lrrecse	|- R Se No

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	|- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
2		df-se	|- ( R Se No <-> A. a e. No { b e. No | b R a } e. _V )
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		fvex	|- ( _L ` a ) e. _V
11		fvex	|- ( _R ` a ) e. _V
12	10 11	unex	|- ( ( _L ` a ) u. ( _R ` a ) ) e. _V
13	12	inex1	|- ( ( ( _L ` a ) u. ( _R ` a ) ) i^i No ) e. _V
14	9 13	eqeltri	|- { b e. No | b e. ( ( _L ` a ) u. ( _R ` a ) ) } e. _V
15	5 14	eqeltrdi	|- ( a e. No -> { b e. No | b R a } e. _V )
16	2 15	mprgbir	|- R Se No