Step |
Hyp |
Ref |
Expression |
1 |
|
df-right |
⊢ R = ( 𝑥 ∈ No ↦ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ) |
2 |
|
bdayelon |
⊢ ( bday ‘ 𝑥 ) ∈ On |
3 |
|
oldf |
⊢ O : On ⟶ 𝒫 No |
4 |
3
|
ffvelrni |
⊢ ( ( bday ‘ 𝑥 ) ∈ On → ( O ‘ ( bday ‘ 𝑥 ) ) ∈ 𝒫 No ) |
5 |
2 4
|
mp1i |
⊢ ( 𝑥 ∈ No → ( O ‘ ( bday ‘ 𝑥 ) ) ∈ 𝒫 No ) |
6 |
5
|
elpwid |
⊢ ( 𝑥 ∈ No → ( O ‘ ( bday ‘ 𝑥 ) ) ⊆ No ) |
7 |
6
|
sselda |
⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ) → 𝑦 ∈ No ) |
8 |
7
|
a1d |
⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ) → ( 𝑥 <s 𝑦 → 𝑦 ∈ No ) ) |
9 |
8
|
ralrimiva |
⊢ ( 𝑥 ∈ No → ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( 𝑥 <s 𝑦 → 𝑦 ∈ No ) ) |
10 |
|
fvex |
⊢ ( O ‘ ( bday ‘ 𝑥 ) ) ∈ V |
11 |
10
|
rabex |
⊢ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ V |
12 |
11
|
elpw |
⊢ ( { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ 𝒫 No ↔ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ⊆ No ) |
13 |
|
rabss |
⊢ ( { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ⊆ No ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( 𝑥 <s 𝑦 → 𝑦 ∈ No ) ) |
14 |
12 13
|
bitri |
⊢ ( { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ 𝒫 No ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( 𝑥 <s 𝑦 → 𝑦 ∈ No ) ) |
15 |
9 14
|
sylibr |
⊢ ( 𝑥 ∈ No → { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ 𝒫 No ) |
16 |
1 15
|
fmpti |
⊢ R : No ⟶ 𝒫 No |