Metamath Proof Explorer

Theorem naddov2

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

Ref Expression
Assertion naddov2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 naddov ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } )
2 snssi ⊢ ( 𝐴 ∈ On → { 𝐴 } ⊆ On )
3 onss ⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
4 xpss12 ⊢ ( ( { 𝐴 } ⊆ On ∧ 𝐵 ⊆ On ) → ( { 𝐴 } × 𝐵 ) ⊆ ( On × On ) )
5 2 3 4 syl2an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( { 𝐴 } × 𝐵 ) ⊆ ( On × On ) )
6 naddfn ⊢ +no Fn ( On × On )
7 6 fndmi ⊢ dom +no = ( On × On )
8 5 7 sseqtrrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( { 𝐴 } × 𝐵 ) ⊆ dom +no )
9 fnfun ⊢ ( +no Fn ( On × On ) → Fun +no )
10 6 9 ax-mp ⊢ Fun +no
11 funimassov ⊢ ( ( Fun +no ∧ ( { 𝐴 } × 𝐵 ) ⊆ dom +no ) → ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ↔ ∀ 𝑡 ∈ { 𝐴 } ∀ 𝑦 ∈ 𝐵 ( 𝑡 +no 𝑦 ) ∈ 𝑥 ) )
12 10 11 mpan ⊢ ( ( { 𝐴 } × 𝐵 ) ⊆ dom +no → ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ↔ ∀ 𝑡 ∈ { 𝐴 } ∀ 𝑦 ∈ 𝐵 ( 𝑡 +no 𝑦 ) ∈ 𝑥 ) )
13 8 12 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ↔ ∀ 𝑡 ∈ { 𝐴 } ∀ 𝑦 ∈ 𝐵 ( 𝑡 +no 𝑦 ) ∈ 𝑥 ) )
14 oveq1 ⊢ ( 𝑡 = 𝐴 → ( 𝑡 +no 𝑦 ) = ( 𝐴 +no 𝑦 ) )
15 14 eleq1d ⊢ ( 𝑡 = 𝐴 → ( ( 𝑡 +no 𝑦 ) ∈ 𝑥 ↔ ( 𝐴 +no 𝑦 ) ∈ 𝑥 ) )
16 15 ralbidv ⊢ ( 𝑡 = 𝐴 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑡 +no 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ) )
17 16 ralsng ⊢ ( 𝐴 ∈ On → ( ∀ 𝑡 ∈ { 𝐴 } ∀ 𝑦 ∈ 𝐵 ( 𝑡 +no 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ) )
18 17 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∀ 𝑡 ∈ { 𝐴 } ∀ 𝑦 ∈ 𝐵 ( 𝑡 +no 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ) )
19 13 18 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ) )
20 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
21 snssi ⊢ ( 𝐵 ∈ On → { 𝐵 } ⊆ On )
22 xpss12 ⊢ ( ( 𝐴 ⊆ On ∧ { 𝐵 } ⊆ On ) → ( 𝐴 × { 𝐵 } ) ⊆ ( On × On ) )
23 20 21 22 syl2an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 × { 𝐵 } ) ⊆ ( On × On ) )
24 23 7 sseqtrrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 × { 𝐵 } ) ⊆ dom +no )
25 funimassov ⊢ ( ( Fun +no ∧ ( 𝐴 × { 𝐵 } ) ⊆ dom +no ) → ( ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ { 𝐵 } ( 𝑧 +no 𝑡 ) ∈ 𝑥 ) )
26 10 25 mpan ⊢ ( ( 𝐴 × { 𝐵 } ) ⊆ dom +no → ( ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ { 𝐵 } ( 𝑧 +no 𝑡 ) ∈ 𝑥 ) )
27 24 26 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ { 𝐵 } ( 𝑧 +no 𝑡 ) ∈ 𝑥 ) )
28 oveq2 ⊢ ( 𝑡 = 𝐵 → ( 𝑧 +no 𝑡 ) = ( 𝑧 +no 𝐵 ) )
29 28 eleq1d ⊢ ( 𝑡 = 𝐵 → ( ( 𝑧 +no 𝑡 ) ∈ 𝑥 ↔ ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) )
30 29 ralsng ⊢ ( 𝐵 ∈ On → ( ∀ 𝑡 ∈ { 𝐵 } ( 𝑧 +no 𝑡 ) ∈ 𝑥 ↔ ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) )
31 30 ralbidv ⊢ ( 𝐵 ∈ On → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ { 𝐵 } ( 𝑧 +no 𝑡 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) )
32 31 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ { 𝐵 } ( 𝑧 +no 𝑡 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) )
33 27 32 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) )
34 19 33 anbi12d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) ) )
35 34 rabbidv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) } )
36 35 inteqd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) } )
37 1 36 eqtrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝐵 ) ∈ 𝑥 ) } )