Metamath Proof Explorer

Theorem nadd1suc

Description: Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024)

Ref Expression
Assertion nadd1suc ( 𝐴 ∈ On → ( 𝐴 +no 1o ) = suc 𝐴 )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 +no 1o ) = ( 𝑏 +no 1o ) )
2 suceq ⊢ ( 𝑎 = 𝑏 → suc 𝑎 = suc 𝑏 )
3 1 2 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 +no 1o ) = suc 𝑎 ↔ ( 𝑏 +no 1o ) = suc 𝑏 ) )
4 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no 1o ) = ( 𝐴 +no 1o ) )
5 suceq ⊢ ( 𝑎 = 𝐴 → suc 𝑎 = suc 𝐴 )
6 4 5 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no 1o ) = suc 𝑎 ↔ ( 𝐴 +no 1o ) = suc 𝐴 ) )
7 naddrid ⊢ ( 𝑎 ∈ On → ( 𝑎 +no ∅ ) = 𝑎 )
8 7 eleq1d ⊢ ( 𝑎 ∈ On → ( ( 𝑎 +no ∅ ) ∈ 𝑥 ↔ 𝑎 ∈ 𝑥 ) )
9 8 anbi1d ⊢ ( 𝑎 ∈ On → ( ( ( 𝑎 +no ∅ ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ↔ ( 𝑎 ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ) )
10 9 ad2antrr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) ∧ 𝑥 ∈ On ) → ( ( ( 𝑎 +no ∅ ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ↔ ( 𝑎 ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ) )
11 df1o2 ⊢ 1o = { ∅ }
12 11 raleqi ⊢ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ { ∅ } ( 𝑎 +no 𝑦 ) ∈ 𝑥 )
13 0ex ⊢ ∅ ∈ V
14 oveq2 ⊢ ( 𝑦 = ∅ → ( 𝑎 +no 𝑦 ) = ( 𝑎 +no ∅ ) )
15 14 eleq1d ⊢ ( 𝑦 = ∅ → ( ( 𝑎 +no 𝑦 ) ∈ 𝑥 ↔ ( 𝑎 +no ∅ ) ∈ 𝑥 ) )
16 13 15 ralsn ⊢ ( ∀ 𝑦 ∈ { ∅ } ( 𝑎 +no 𝑦 ) ∈ 𝑥 ↔ ( 𝑎 +no ∅ ) ∈ 𝑥 )
17 12 16 bitri ⊢ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ↔ ( 𝑎 +no ∅ ) ∈ 𝑥 )
18 17 a1i ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ↔ ( 𝑎 +no ∅ ) ∈ 𝑥 ) )
19 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 +no 1o ) = ( 𝑏 +no 1o ) )
20 19 eleq1d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑦 +no 1o ) ∈ 𝑥 ↔ ( 𝑏 +no 1o ) ∈ 𝑥 ) )
21 20 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) ∈ 𝑥 )
22 nfv ⊢ Ⅎ 𝑏 𝑎 ∈ On
23 nfra1 ⊢ Ⅎ 𝑏 ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏
24 22 23 nfan ⊢ Ⅎ 𝑏 ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 )
25 simpr ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 )
26 25 r19.21bi ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) ∧ 𝑏 ∈ 𝑎 ) → ( 𝑏 +no 1o ) = suc 𝑏 )
27 26 eleq1d ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) ∧ 𝑏 ∈ 𝑎 ) → ( ( 𝑏 +no 1o ) ∈ 𝑥 ↔ suc 𝑏 ∈ 𝑥 ) )
28 24 27 ralbida ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) )
29 21 28 bitrid ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ( ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) )
30 18 29 anbi12d ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ( ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) ↔ ( ( 𝑎 +no ∅ ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ) )
31 30 adantr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) ↔ ( ( 𝑎 +no ∅ ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ) )
32 onelon ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ On )
33 32 ad4ant13 ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → 𝑏 ∈ On )
34 onsuc ⊢ ( 𝑏 ∈ On → suc 𝑏 ∈ On )
35 33 34 syl ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → suc 𝑏 ∈ On )
36 simpllr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → 𝑥 ∈ On )
37 35 36 jca ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → ( suc 𝑏 ∈ On ∧ 𝑥 ∈ On ) )
38 eloni ⊢ ( 𝑎 ∈ On → Ord 𝑎 )
39 38 ad3antrrr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → Ord 𝑎 )
40 simplr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → 𝑏 ∈ 𝑎 )
41 ordsucss ⊢ ( Ord 𝑎 → ( 𝑏 ∈ 𝑎 → suc 𝑏 ⊆ 𝑎 ) )
42 39 40 41 sylc ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → suc 𝑏 ⊆ 𝑎 )
43 simpr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → 𝑎 ∈ 𝑥 )
44 42 43 jca ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → ( suc 𝑏 ⊆ 𝑎 ∧ 𝑎 ∈ 𝑥 ) )
45 ontr2 ⊢ ( ( suc 𝑏 ∈ On ∧ 𝑥 ∈ On ) → ( ( suc 𝑏 ⊆ 𝑎 ∧ 𝑎 ∈ 𝑥 ) → suc 𝑏 ∈ 𝑥 ) )
46 37 44 45 sylc ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) ∧ 𝑎 ∈ 𝑥 ) → suc 𝑏 ∈ 𝑥 )
47 46 ex ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) → ( 𝑎 ∈ 𝑥 → suc 𝑏 ∈ 𝑥 ) )
48 47 ralrimdva ⊢ ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑎 ∈ 𝑥 → ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) )
49 48 pm4.71d ⊢ ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑎 ∈ 𝑥 ↔ ( 𝑎 ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ) )
50 49 adantlr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) ∧ 𝑥 ∈ On ) → ( 𝑎 ∈ 𝑥 ↔ ( 𝑎 ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥 ) ) )
51 10 31 50 3bitr4d ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) ↔ 𝑎 ∈ 𝑥 ) )
52 51 rabbidva ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) } = { 𝑥 ∈ On ∣ 𝑎 ∈ 𝑥 } )
53 52 inteqd ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ 𝑎 ∈ 𝑥 } )
54 1on ⊢ 1o ∈ On
55 naddov2 ⊢ ( ( 𝑎 ∈ On ∧ 1o ∈ On ) → ( 𝑎 +no 1o ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) } )
56 54 55 mpan2 ⊢ ( 𝑎 ∈ On → ( 𝑎 +no 1o ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) } )
57 56 adantr ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ( 𝑎 +no 1o ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 1o ( 𝑎 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑎 ( 𝑦 +no 1o ) ∈ 𝑥 ) } )
58 onsucmin ⊢ ( 𝑎 ∈ On → suc 𝑎 = ∩ { 𝑥 ∈ On ∣ 𝑎 ∈ 𝑥 } )
59 58 adantr ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → suc 𝑎 = ∩ { 𝑥 ∈ On ∣ 𝑎 ∈ 𝑥 } )
60 53 57 59 3eqtr4d ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 ) → ( 𝑎 +no 1o ) = suc 𝑎 )
61 60 ex ⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no 1o ) = suc 𝑏 → ( 𝑎 +no 1o ) = suc 𝑎 ) )
62 3 6 61 tfis3 ⊢ ( 𝐴 ∈ On → ( 𝐴 +no 1o ) = suc 𝐴 )