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	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion	lrrecse	⊢ 𝑅 Se No

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
2		df-se	⊢ ( 𝑅 Se No ↔ ∀ 𝑎 ∈ No { 𝑏 ∈ No ∣ 𝑏 𝑅 𝑎 } ∈ V )
3	1	lrrecval	⊢ ( ( 𝑏 ∈ No ∧ 𝑎 ∈ No ) → ( 𝑏 𝑅 𝑎 ↔ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ) )
4	3	ancoms	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ) → ( 𝑏 𝑅 𝑎 ↔ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ) )
5	4	rabbidva	⊢ ( 𝑎 ∈ No → { 𝑏 ∈ No ∣ 𝑏 𝑅 𝑎 } = { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } )
6		dfrab2	⊢ { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } = ( { 𝑏 ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } ∩ No )
7		abid2	⊢ { 𝑏 ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } = ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) )
8	7	ineq1i	⊢ ( { 𝑏 ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } ∩ No ) = ( ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∩ No )
9	6 8	eqtri	⊢ { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } = ( ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∩ No )
10		fvex	⊢ ( L ‘ 𝑎 ) ∈ V
11		fvex	⊢ ( R ‘ 𝑎 ) ∈ V
12	10 11	unex	⊢ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∈ V
13	12	inex1	⊢ ( ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∩ No ) ∈ V
14	9 13	eqeltri	⊢ { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) } ∈ V
15	5 14	eqeltrdi	⊢ ( 𝑎 ∈ No → { 𝑏 ∈ No ∣ 𝑏 𝑅 𝑎 } ∈ V )
16	2 15	mprgbir	⊢ 𝑅 Se No