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	No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
Assertion	lrrecse	$$⊢R\mathrm{Se}\mathrm{No}$$

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		df-se	$$⊢R\mathrm{Se}\mathrm{No}\leftrightarrow \forall a\in \mathrm{No}\left\{b\in \mathrm{No}|bRa\right\}\in \mathrm{V}$$
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		fvex	Could not format ( _Left ` a ) e. _V : No typesetting found for |- ( _Left ` a ) e. _V with typecode |-
11		fvex	Could not format ( _Right ` a ) e. _V : No typesetting found for |- ( _Right ` a ) e. _V with typecode |-
12	10 11	unex	Could not format ( ( _Left ` a ) u. ( _Right ` a ) ) e. _V : No typesetting found for |- ( ( _Left ` a ) u. ( _Right ` a ) ) e. _V with typecode |-
13	12	inex1	Could not format ( ( ( _Left ` a ) u. ( _Right ` a ) ) i^i No ) e. _V : No typesetting found for |- ( ( ( _Left ` a ) u. ( _Right ` a ) ) i^i No ) e. _V with typecode |-
14	9 13	eqeltri	Could not format { b e. No | b e. ( ( _Left ` a ) u. ( _Right ` a ) ) } e. _V : No typesetting found for |- { b e. No | b e. ( ( _Left ` a ) u. ( _Right ` a ) ) } e. _V with typecode |-
15	5 14	eqeltrdi	$$⊢a\in \mathrm{No}\to \left\{b\in \mathrm{No}|bRa\right\}\in \mathrm{V}$$
16	2 15	mprgbir	$$⊢R\mathrm{Se}\mathrm{No}$$