Theorem naddov4

Description: Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024)

	Ref	Expression
Assertion	naddov4	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ ( { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		naddov2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 ) } )
2		inrab	⊢ ( { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ) = { 𝑥 ∈ On ∣ ( ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 ) }
3		incom	⊢ ( { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ) = ( { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } )
4	2 3	eqtr3i	⊢ { 𝑥 ∈ On ∣ ( ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 ) } = ( { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } )
5	4	inteqi	⊢ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 ) } = ∩ ( { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } )
6	1 5	eqtrdi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ ( { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝑥 } ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝑥 } ) )