Metamath Proof Explorer


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