| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-made |
⊢ M = recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) |
| 2 |
1
|
tfr1 |
⊢ M Fn On |
| 3 |
|
madeval2 |
⊢ ( 𝑥 ∈ On → ( M ‘ 𝑥 ) = { 𝑦 ∈ No ∣ ∃ 𝑧 ∈ 𝒫 ∪ ( M “ 𝑥 ) ∃ 𝑤 ∈ 𝒫 ∪ ( M “ 𝑥 ) ( 𝑧 <<s 𝑤 ∧ ( 𝑧 |s 𝑤 ) = 𝑦 ) } ) |
| 4 |
|
ssrab2 |
⊢ { 𝑦 ∈ No ∣ ∃ 𝑧 ∈ 𝒫 ∪ ( M “ 𝑥 ) ∃ 𝑤 ∈ 𝒫 ∪ ( M “ 𝑥 ) ( 𝑧 <<s 𝑤 ∧ ( 𝑧 |s 𝑤 ) = 𝑦 ) } ⊆ No |
| 5 |
3 4
|
eqsstrdi |
⊢ ( 𝑥 ∈ On → ( M ‘ 𝑥 ) ⊆ No ) |
| 6 |
|
sseq1 |
⊢ ( 𝑦 = ( M ‘ 𝑥 ) → ( 𝑦 ⊆ No ↔ ( M ‘ 𝑥 ) ⊆ No ) ) |
| 7 |
5 6
|
syl5ibrcom |
⊢ ( 𝑥 ∈ On → ( 𝑦 = ( M ‘ 𝑥 ) → 𝑦 ⊆ No ) ) |
| 8 |
7
|
rexlimiv |
⊢ ( ∃ 𝑥 ∈ On 𝑦 = ( M ‘ 𝑥 ) → 𝑦 ⊆ No ) |
| 9 |
|
vex |
⊢ 𝑦 ∈ V |
| 10 |
|
eqeq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 = ( M ‘ 𝑥 ) ↔ 𝑦 = ( M ‘ 𝑥 ) ) ) |
| 11 |
10
|
rexbidv |
⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑥 ∈ On 𝑧 = ( M ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝑦 = ( M ‘ 𝑥 ) ) ) |
| 12 |
|
fnrnfv |
⊢ ( M Fn On → ran M = { 𝑧 ∣ ∃ 𝑥 ∈ On 𝑧 = ( M ‘ 𝑥 ) } ) |
| 13 |
2 12
|
ax-mp |
⊢ ran M = { 𝑧 ∣ ∃ 𝑥 ∈ On 𝑧 = ( M ‘ 𝑥 ) } |
| 14 |
9 11 13
|
elab2 |
⊢ ( 𝑦 ∈ ran M ↔ ∃ 𝑥 ∈ On 𝑦 = ( M ‘ 𝑥 ) ) |
| 15 |
|
velpw |
⊢ ( 𝑦 ∈ 𝒫 No ↔ 𝑦 ⊆ No ) |
| 16 |
8 14 15
|
3imtr4i |
⊢ ( 𝑦 ∈ ran M → 𝑦 ∈ 𝒫 No ) |
| 17 |
16
|
ssriv |
⊢ ran M ⊆ 𝒫 No |
| 18 |
|
df-f |
⊢ ( M : On ⟶ 𝒫 No ↔ ( M Fn On ∧ ran M ⊆ 𝒫 No ) ) |
| 19 |
2 17 18
|
mpbir2an |
⊢ M : On ⟶ 𝒫 No |