Description: The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | naddov | ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | naddcllem | ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +no 𝐵 ) ∈ On ∧ ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) ) | |
2 | 1 | simprd | ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) |