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 |