| Step |
Hyp |
Ref |
Expression |
| 1 |
|
addsfn |
⊢ +s Fn ( No × No ) |
| 2 |
|
addscl |
⊢ ( ( 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( 𝑦 +s 𝑧 ) ∈ No ) |
| 3 |
2
|
rgen2 |
⊢ ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( 𝑦 +s 𝑧 ) ∈ No |
| 4 |
|
fveq2 |
⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( +s ‘ 𝑥 ) = ( +s ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) |
| 5 |
|
df-ov |
⊢ ( 𝑦 +s 𝑧 ) = ( +s ‘ ⟨ 𝑦 , 𝑧 ⟩ ) |
| 6 |
4 5
|
eqtr4di |
⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( +s ‘ 𝑥 ) = ( 𝑦 +s 𝑧 ) ) |
| 7 |
6
|
eleq1d |
⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( +s ‘ 𝑥 ) ∈ No ↔ ( 𝑦 +s 𝑧 ) ∈ No ) ) |
| 8 |
7
|
ralxp |
⊢ ( ∀ 𝑥 ∈ ( No × No ) ( +s ‘ 𝑥 ) ∈ No ↔ ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( 𝑦 +s 𝑧 ) ∈ No ) |
| 9 |
3 8
|
mpbir |
⊢ ∀ 𝑥 ∈ ( No × No ) ( +s ‘ 𝑥 ) ∈ No |
| 10 |
|
ffnfv |
⊢ ( +s : ( No × No ) ⟶ No ↔ ( +s Fn ( No × No ) ∧ ∀ 𝑥 ∈ ( No × No ) ( +s ‘ 𝑥 ) ∈ No ) ) |
| 11 |
1 9 10
|
mpbir2an |
⊢ +s : ( No × No ) ⟶ No |