Metamath Proof Explorer

Theorem naddov2

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

Ref Expression
Assertion naddov2 
|- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } )

Proof

Step Hyp Ref Expression
1 naddov 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } )
2 snssi 
 |-  ( A e. On -> { A } C_ On )
3 onss 
 |-  ( B e. On -> B C_ On )
4 xpss12 
 |-  ( ( { A } C_ On /\ B C_ On ) -> ( { A } X. B ) C_ ( On X. On ) )
5 2 3 4 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> ( { A } X. B ) C_ ( On X. On ) )
6 naddfn 
 |-  +no Fn ( On X. On )
7 6 fndmi 
 |-  dom +no = ( On X. On )
8 5 7 sseqtrrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( { A } X. B ) C_ dom +no )
9 fnfun 
 |-  ( +no Fn ( On X. On ) -> Fun +no )
10 6 9 ax-mp 
 |-  Fun +no
11 funimassov 
 |-  ( ( Fun +no /\ ( { A } X. B ) C_ dom +no ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) )
12 10 11 mpan 
 |-  ( ( { A } X. B ) C_ dom +no -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) )
13 8 12 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) )
14 oveq1 
 |-  ( t = A -> ( t +no y ) = ( A +no y ) )
15 14 eleq1d 
 |-  ( t = A -> ( ( t +no y ) e. x <-> ( A +no y ) e. x ) )
16 15 ralbidv 
 |-  ( t = A -> ( A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) )
17 16 ralsng 
 |-  ( A e. On -> ( A. t e. { A } A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) )
18 17 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( A. t e. { A } A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) )
19 13 18 bitrd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. y e. B ( A +no y ) e. x ) )
20 onss 
 |-  ( A e. On -> A C_ On )
21 snssi 
 |-  ( B e. On -> { B } C_ On )
22 xpss12 
 |-  ( ( A C_ On /\ { B } C_ On ) -> ( A X. { B } ) C_ ( On X. On ) )
23 20 21 22 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> ( A X. { B } ) C_ ( On X. On ) )
24 23 7 sseqtrrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( A X. { B } ) C_ dom +no )
25 funimassov 
 |-  ( ( Fun +no /\ ( A X. { B } ) C_ dom +no ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) )
26 10 25 mpan 
 |-  ( ( A X. { B } ) C_ dom +no -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) )
27 24 26 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) )
28 oveq2 
 |-  ( t = B -> ( z +no t ) = ( z +no B ) )
29 28 eleq1d 
 |-  ( t = B -> ( ( z +no t ) e. x <-> ( z +no B ) e. x ) )
30 29 ralsng 
 |-  ( B e. On -> ( A. t e. { B } ( z +no t ) e. x <-> ( z +no B ) e. x ) )
31 30 ralbidv 
 |-  ( B e. On -> ( A. z e. A A. t e. { B } ( z +no t ) e. x <-> A. z e. A ( z +no B ) e. x ) )
32 31 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( A. z e. A A. t e. { B } ( z +no t ) e. x <-> A. z e. A ( z +no B ) e. x ) )
33 27 32 bitrd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A ( z +no B ) e. x ) )
34 19 33 anbi12d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) <-> ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) ) )
35 34 rabbidv 
 |-  ( ( A e. On /\ B e. On ) -> { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } )
36 35 inteqd 
 |-  ( ( A e. On /\ B e. On ) -> |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } )
37 1 36 eqtrd 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } )