Metamath Proof Explorer

Theorem nadd1suc

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

Ref Expression
Assertion nadd1suc ⊢ A ∈ On → A + 1 𝑜 = suc ⁡ A

Proof

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