Metamath Proof Explorer


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 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion lrrecpred ( 𝐴 No → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 lrrec.1 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
2 dfpred3g ( 𝐴 No → Pred ( 𝑅 , No , 𝐴 ) = { 𝑏 No 𝑏 𝑅 𝐴 } )
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 5 9 eqtrdi ( 𝐴 No → { 𝑏 No 𝑏 𝑅 𝐴 } = ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) )
11 leftssno ( L ‘ 𝐴 ) ⊆ No
12 11 a1i ( 𝐴 No → ( L ‘ 𝐴 ) ⊆ No )
13 rightssno ( R ‘ 𝐴 ) ⊆ No
14 13 a1i ( 𝐴 No → ( R ‘ 𝐴 ) ⊆ No )
15 12 14 unssd ( 𝐴 No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No )
16 df-ss ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No ↔ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
17 15 16 sylib ( 𝐴 No → ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
18 2 10 17 3eqtrd ( 𝐴 No → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )