Metamath Proof Explorer


Theorem naddov

Description: The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddov ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 naddcllem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +no 𝐵 ) ∈ On ∧ ( 𝐴 +no 𝐵 ) = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) )
2 1 simprd ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } )