Metamath Proof Explorer

Theorem naddid1

Description: Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddid1 
|- ( A e. On -> ( A +no (/) ) = A )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = b -> ( a +no (/) ) = ( b +no (/) ) )
2 id 
 |-  ( a = b -> a = b )
3 1 2 eqeq12d 
 |-  ( a = b -> ( ( a +no (/) ) = a <-> ( b +no (/) ) = b ) )
4 oveq1 
 |-  ( a = A -> ( a +no (/) ) = ( A +no (/) ) )
5 id 
 |-  ( a = A -> a = A )
6 4 5 eqeq12d 
 |-  ( a = A -> ( ( a +no (/) ) = a <-> ( A +no (/) ) = A ) )
7 0elon 
 |-  (/) e. On
8 naddov2 
 |-  ( ( a e. On /\ (/) e. On ) -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } )
9 7 8 mpan2 
 |-  ( a e. On -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } )
10 9 adantr 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } )
11 ral0 
 |-  A. c e. (/) ( a +no c ) e. x
12 11 biantrur 
 |-  ( A. b e. a ( b +no (/) ) e. x <-> ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) )
13 eleq1 
 |-  ( ( b +no (/) ) = b -> ( ( b +no (/) ) e. x <-> b e. x ) )
14 13 ralimi 
 |-  ( A. b e. a ( b +no (/) ) = b -> A. b e. a ( ( b +no (/) ) e. x <-> b e. x ) )
15 ralbi 
 |-  ( A. b e. a ( ( b +no (/) ) e. x <-> b e. x ) -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) )
16 14 15 syl 
 |-  ( A. b e. a ( b +no (/) ) = b -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) )
17 16 adantl 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) )
18 dfss3 
 |-  ( a C_ x <-> A. b e. a b e. x )
19 17 18 bitr4di 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( A. b e. a ( b +no (/) ) e. x <-> a C_ x ) )
20 12 19 bitr3id 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) <-> a C_ x ) )
21 20 rabbidv 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } = { x e. On | a C_ x } )
22 21 inteqd 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } = |^| { x e. On | a C_ x } )
23 intmin 
 |-  ( a e. On -> |^| { x e. On | a C_ x } = a )
24 23 adantr 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> |^| { x e. On | a C_ x } = a )
25 10 22 24 3eqtrd 
 |-  ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( a +no (/) ) = a )
26 25 ex 
 |-  ( a e. On -> ( A. b e. a ( b +no (/) ) = b -> ( a +no (/) ) = a ) )
27 3 6 26 tfis3 
 |-  ( A e. On -> ( A +no (/) ) = A )