Metamath Proof Explorer

Theorem naddov2

Description: Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddov2 ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ x ∈ On | ∀ y ∈ B A + y ∈ x ∧ ∀ z ∈ A z + B ∈ x

Proof

Step Hyp Ref Expression
1 naddov ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ x ∈ On | + A × B ⊆ x ∧ + A × B ⊆ x
2 snssi ⊢ A ∈ On → A ⊆ On
3 onss ⊢ B ∈ On → B ⊆ On
4 xpss12 ⊢ A ⊆ On ∧ B ⊆ On → A × B ⊆ On × On
5 2 3 4 syl2an ⊢ A ∈ On ∧ B ∈ On → A × B ⊆ On × On
6 naddfn ⊢ + Fn On × On
7 6 fndmi ⊢ dom ⁡ + = On × On
8 5 7 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On → A × B ⊆ dom ⁡ +
9 fnfun ⊢ + Fn On × On → Fun ⁡ +
10 6 9 ax-mp ⊢ Fun ⁡ +
11 funimassov ⊢ Fun ⁡ + ∧ A × B ⊆ dom ⁡ + → + A × B ⊆ x ↔ ∀ t ∈ A ∀ y ∈ B t + y ∈ x
12 10 11 mpan ⊢ A × B ⊆ dom ⁡ + → + A × B ⊆ x ↔ ∀ t ∈ A ∀ y ∈ B t + y ∈ x
13 8 12 syl ⊢ A ∈ On ∧ B ∈ On → + A × B ⊆ x ↔ ∀ t ∈ A ∀ y ∈ B t + y ∈ x
14 oveq1 ⊢ t = A → t + y = A + y
15 14 eleq1d ⊢ t = A → t + y ∈ x ↔ A + y ∈ x
16 15 ralbidv ⊢ t = A → ∀ y ∈ B t + y ∈ x ↔ ∀ y ∈ B A + y ∈ x
17 16 ralsng ⊢ A ∈ On → ∀ t ∈ A ∀ y ∈ B t + y ∈ x ↔ ∀ y ∈ B A + y ∈ x
18 17 adantr ⊢ A ∈ On ∧ B ∈ On → ∀ t ∈ A ∀ y ∈ B t + y ∈ x ↔ ∀ y ∈ B A + y ∈ x
19 13 18 bitrd ⊢ A ∈ On ∧ B ∈ On → + A × B ⊆ x ↔ ∀ y ∈ B A + y ∈ x
20 onss ⊢ A ∈ On → A ⊆ On
21 snssi ⊢ B ∈ On → B ⊆ On
22 xpss12 ⊢ A ⊆ On ∧ B ⊆ On → A × B ⊆ On × On
23 20 21 22 syl2an ⊢ A ∈ On ∧ B ∈ On → A × B ⊆ On × On
24 23 7 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On → A × B ⊆ dom ⁡ +
25 funimassov ⊢ Fun ⁡ + ∧ A × B ⊆ dom ⁡ + → + A × B ⊆ x ↔ ∀ z ∈ A ∀ t ∈ B z + t ∈ x
26 10 25 mpan ⊢ A × B ⊆ dom ⁡ + → + A × B ⊆ x ↔ ∀ z ∈ A ∀ t ∈ B z + t ∈ x
27 24 26 syl ⊢ A ∈ On ∧ B ∈ On → + A × B ⊆ x ↔ ∀ z ∈ A ∀ t ∈ B z + t ∈ x
28 oveq2 ⊢ t = B → z + t = z + B
29 28 eleq1d ⊢ t = B → z + t ∈ x ↔ z + B ∈ x
30 29 ralsng ⊢ B ∈ On → ∀ t ∈ B z + t ∈ x ↔ z + B ∈ x
31 30 ralbidv ⊢ B ∈ On → ∀ z ∈ A ∀ t ∈ B z + t ∈ x ↔ ∀ z ∈ A z + B ∈ x
32 31 adantl ⊢ A ∈ On ∧ B ∈ On → ∀ z ∈ A ∀ t ∈ B z + t ∈ x ↔ ∀ z ∈ A z + B ∈ x
33 27 32 bitrd ⊢ A ∈ On ∧ B ∈ On → + A × B ⊆ x ↔ ∀ z ∈ A z + B ∈ x
34 19 33 anbi12d ⊢ A ∈ On ∧ B ∈ On → + A × B ⊆ x ∧ + A × B ⊆ x ↔ ∀ y ∈ B A + y ∈ x ∧ ∀ z ∈ A z + B ∈ x
35 34 rabbidv ⊢ A ∈ On ∧ B ∈ On → x ∈ On | + A × B ⊆ x ∧ + A × B ⊆ x = x ∈ On | ∀ y ∈ B A + y ∈ x ∧ ∀ z ∈ A z + B ∈ x
36 35 inteqd ⊢ A ∈ On ∧ B ∈ On → ⋂ x ∈ On | + A × B ⊆ x ∧ + A × B ⊆ x = ⋂ x ∈ On | ∀ y ∈ B A + y ∈ x ∧ ∀ z ∈ A z + B ∈ x
37 1 36 eqtrd ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ x ∈ On | ∀ y ∈ B A + y ∈ x ∧ ∀ z ∈ A z + B ∈ x