Theorem naddov3

Description: Alternate expression for natural addition. (Contributed by Scott Fenton, 20-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		naddov	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } )
2		unss	⊢ ( ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ∪ ( +no “ ( 𝐴 × { 𝐵 } ) ) ) ⊆ 𝑥 )
3	2	rabbii	⊢ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ∪ ( +no “ ( 𝐴 × { 𝐵 } ) ) ) ⊆ 𝑥 }
4	3	inteqi	⊢ ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ∪ ( +no “ ( 𝐴 × { 𝐵 } ) ) ) ⊆ 𝑥 }
5	1 4	eqtrdi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ∪ ( +no “ ( 𝐴 × { 𝐵 } ) ) ) ⊆ 𝑥 } )