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 ‘ 𝐴 ) ) ) |