Metamath Proof Explorer

Theorem naddov4

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

Ref Expression
Assertion naddov4 ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ x ∈ On | ∀ a ∈ A a + B ∈ x ∩ x ∈ On | ∀ b ∈ B A + b ∈ x

Proof

Step Hyp Ref Expression
1 naddov2 ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ x ∈ On | ∀ b ∈ B A + b ∈ x ∧ ∀ a ∈ A a + B ∈ x
2 inrab ⊢ x ∈ On | ∀ b ∈ B A + b ∈ x ∩ x ∈ On | ∀ a ∈ A a + B ∈ x = x ∈ On | ∀ b ∈ B A + b ∈ x ∧ ∀ a ∈ A a + B ∈ x
3 incom ⊢ x ∈ On | ∀ b ∈ B A + b ∈ x ∩ x ∈ On | ∀ a ∈ A a + B ∈ x = x ∈ On | ∀ a ∈ A a + B ∈ x ∩ x ∈ On | ∀ b ∈ B A + b ∈ x
4 2 3 eqtr3i ⊢ x ∈ On | ∀ b ∈ B A + b ∈ x ∧ ∀ a ∈ A a + B ∈ x = x ∈ On | ∀ a ∈ A a + B ∈ x ∩ x ∈ On | ∀ b ∈ B A + b ∈ x
5 4 inteqi ⊢ ⋂ x ∈ On | ∀ b ∈ B A + b ∈ x ∧ ∀ a ∈ A a + B ∈ x = ⋂ x ∈ On | ∀ a ∈ A a + B ∈ x ∩ x ∈ On | ∀ b ∈ B A + b ∈ x
6 1 5 eqtrdi ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ x ∈ On | ∀ a ∈ A a + B ∈ x ∩ x ∈ On | ∀ b ∈ B A + b ∈ x