Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  naddsuc2 Structured version   Visualization version   GIF version

Theorem naddsuc2 42598
Description: Natural addition with successor. (Contributed by RP, 1-Jan-2025.)
Assertion
Ref Expression
naddsuc2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵))

Proof of Theorem naddsuc2
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7408 . . 3 (𝑎 = 𝑐 → (𝑎 +no suc 𝑏) = (𝑐 +no suc 𝑏))
2 oveq1 7408 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
3 suceq 6420 . . . 4 ((𝑎 +no 𝑏) = (𝑐 +no 𝑏) → suc (𝑎 +no 𝑏) = suc (𝑐 +no 𝑏))
42, 3syl 17 . . 3 (𝑎 = 𝑐 → suc (𝑎 +no 𝑏) = suc (𝑐 +no 𝑏))
51, 4eqeq12d 2740 . 2 (𝑎 = 𝑐 → ((𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏) ↔ (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)))
6 suceq 6420 . . . 4 (𝑏 = 𝑑 → suc 𝑏 = suc 𝑑)
76oveq2d 7417 . . 3 (𝑏 = 𝑑 → (𝑐 +no suc 𝑏) = (𝑐 +no suc 𝑑))
8 oveq2 7409 . . . 4 (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
9 suceq 6420 . . . 4 ((𝑐 +no 𝑏) = (𝑐 +no 𝑑) → suc (𝑐 +no 𝑏) = suc (𝑐 +no 𝑑))
108, 9syl 17 . . 3 (𝑏 = 𝑑 → suc (𝑐 +no 𝑏) = suc (𝑐 +no 𝑑))
117, 10eqeq12d 2740 . 2 (𝑏 = 𝑑 → ((𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ↔ (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑)))
12 oveq1 7408 . . 3 (𝑎 = 𝑐 → (𝑎 +no suc 𝑑) = (𝑐 +no suc 𝑑))
13 oveq1 7408 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
14 suceq 6420 . . . 4 ((𝑎 +no 𝑑) = (𝑐 +no 𝑑) → suc (𝑎 +no 𝑑) = suc (𝑐 +no 𝑑))
1513, 14syl 17 . . 3 (𝑎 = 𝑐 → suc (𝑎 +no 𝑑) = suc (𝑐 +no 𝑑))
1612, 15eqeq12d 2740 . 2 (𝑎 = 𝑐 → ((𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑) ↔ (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑)))
17 oveq1 7408 . . 3 (𝑎 = 𝐴 → (𝑎 +no suc 𝑏) = (𝐴 +no suc 𝑏))
18 oveq1 7408 . . . 4 (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
19 suceq 6420 . . . 4 ((𝑎 +no 𝑏) = (𝐴 +no 𝑏) → suc (𝑎 +no 𝑏) = suc (𝐴 +no 𝑏))
2018, 19syl 17 . . 3 (𝑎 = 𝐴 → suc (𝑎 +no 𝑏) = suc (𝐴 +no 𝑏))
2117, 20eqeq12d 2740 . 2 (𝑎 = 𝐴 → ((𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏) ↔ (𝐴 +no suc 𝑏) = suc (𝐴 +no 𝑏)))
22 suceq 6420 . . . 4 (𝑏 = 𝐵 → suc 𝑏 = suc 𝐵)
2322oveq2d 7417 . . 3 (𝑏 = 𝐵 → (𝐴 +no suc 𝑏) = (𝐴 +no suc 𝐵))
24 oveq2 7409 . . . 4 (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
25 suceq 6420 . . . 4 ((𝐴 +no 𝑏) = (𝐴 +no 𝐵) → suc (𝐴 +no 𝑏) = suc (𝐴 +no 𝐵))
2624, 25syl 17 . . 3 (𝑏 = 𝐵 → suc (𝐴 +no 𝑏) = suc (𝐴 +no 𝐵))
2723, 26eqeq12d 2740 . 2 (𝑏 = 𝐵 → ((𝐴 +no suc 𝑏) = suc (𝐴 +no 𝑏) ↔ (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵)))
28 simp2 1134 . . . 4 ((∀𝑐𝑎𝑑𝑏 (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ∧ ∀𝑑𝑏 (𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑)) → ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
2928a1i 11 . . 3 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐𝑎𝑑𝑏 (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ∧ ∀𝑑𝑏 (𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑)) → ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)))
30 df-suc 6360 . . . . . . . . . . . 12 suc 𝑏 = (𝑏 ∪ {𝑏})
3130a1i 11 . . . . . . . . . . 11 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → suc 𝑏 = (𝑏 ∪ {𝑏}))
3231raleqdv 3317 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ↔ ∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥))
33 vex 3470 . . . . . . . . . . . . 13 𝑏 ∈ V
3433a1i 11 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → 𝑏 ∈ V)
35 oveq2 7409 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 → (𝑎 +no 𝑑) = (𝑎 +no 𝑏))
3635eleq1d 2810 . . . . . . . . . . . . 13 (𝑑 = 𝑏 → ((𝑎 +no 𝑑) ∈ 𝑥 ↔ (𝑎 +no 𝑏) ∈ 𝑥))
3736ralunsn 4886 . . . . . . . . . . . 12 (𝑏 ∈ V → (∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥 ↔ (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ (𝑎 +no 𝑏) ∈ 𝑥)))
3834, 37syl 17 . . . . . . . . . . 11 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥 ↔ (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ (𝑎 +no 𝑏) ∈ 𝑥)))
3938biancomd 463 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥 ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥)))
4032, 39bitrd 279 . . . . . . . . 9 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥)))
41 nfv 1909 . . . . . . . . . . . 12 𝑐(𝑎 ∈ On ∧ 𝑏 ∈ On)
42 nfra1 3273 . . . . . . . . . . . 12 𝑐𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)
4341, 42nfan 1894 . . . . . . . . . . 11 𝑐((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
44 nfv 1909 . . . . . . . . . . 11 𝑐 𝑥 ∈ On
4543, 44nfan 1894 . . . . . . . . . 10 𝑐(((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On)
46 simplr 766 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
4746r19.21bi 3240 . . . . . . . . . . 11 (((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) ∧ 𝑐𝑎) → (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
4847eleq1d 2810 . . . . . . . . . 10 (((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) ∧ 𝑐𝑎) → ((𝑐 +no suc 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥))
4945, 48ralbida 3259 . . . . . . . . 9 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥 ↔ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))
5040, 49anbi12d 630 . . . . . . . 8 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥) ↔ (((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥) ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)))
51 anass 468 . . . . . . . . 9 ((((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥) ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥) ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)))
52 simpll3 1211 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑥 ∈ On)
53 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑑𝑏)
54 simpll2 1210 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑏 ∈ On)
55 onelon 6379 . . . . . . . . . . . . . . . . . . 19 ((𝑏 ∈ On ∧ 𝑑𝑏) → 𝑑 ∈ On)
5654, 53, 55syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑑 ∈ On)
57 simpll1 1209 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑎 ∈ On)
58 naddel2 8682 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∈ On ∧ 𝑏 ∈ On ∧ 𝑎 ∈ On) → (𝑑𝑏 ↔ (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏)))
5956, 54, 57, 58syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑑𝑏 ↔ (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏)))
6053, 59mpbid 231 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏))
61 simplr 766 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑎 +no 𝑏) ∈ 𝑥)
6260, 61jca 511 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → ((𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥))
63 ontr1 6400 . . . . . . . . . . . . . . 15 (𝑥 ∈ On → (((𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (𝑎 +no 𝑑) ∈ 𝑥))
6452, 62, 63sylc 65 . . . . . . . . . . . . . 14 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑎 +no 𝑑) ∈ 𝑥)
6564ralrimiva 3138 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥)
66 simpll1 1209 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑎 ∈ On)
67 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑐𝑎)
68 onelon 6379 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑐𝑎) → 𝑐 ∈ On)
6966, 67, 68syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑐 ∈ On)
70 simpll2 1210 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑏 ∈ On)
7169, 66, 703jca 1125 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On))
72 naddelim 8680 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑐𝑎 → (𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏)))
7371, 67, 72sylc 65 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏))
74 simplr 766 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑎 +no 𝑏) ∈ 𝑥)
75 elunii 4904 . . . . . . . . . . . . . . . 16 (((𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (𝑐 +no 𝑏) ∈ 𝑥)
7673, 74, 75syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑐 +no 𝑏) ∈ 𝑥)
77 simpll3 1211 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑥 ∈ On)
78 eloni 6364 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ On → Ord 𝑥)
7977, 78syl 17 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → Ord 𝑥)
80 ordsucuniel 7805 . . . . . . . . . . . . . . . 16 (Ord 𝑥 → ((𝑐 +no 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥))
8179, 80syl 17 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → ((𝑐 +no 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥))
8276, 81mpbid 231 . . . . . . . . . . . . . 14 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → suc (𝑐 +no 𝑏) ∈ 𝑥)
8382ralrimiva 3138 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)
8465, 83jca 511 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))
8584ex 412 . . . . . . . . . . 11 ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) → ((𝑎 +no 𝑏) ∈ 𝑥 → (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)))
8685ad4ant124 1170 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((𝑎 +no 𝑏) ∈ 𝑥 → (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)))
8786pm4.71d 561 . . . . . . . . 9 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((𝑎 +no 𝑏) ∈ 𝑥 ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ (∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))))
8851, 87bitr4id 290 . . . . . . . 8 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥) ∧ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥) ↔ (𝑎 +no 𝑏) ∈ 𝑥))
8950, 88bitrd 279 . . . . . . 7 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥) ↔ (𝑎 +no 𝑏) ∈ 𝑥))
9089rabbidva 3431 . . . . . 6 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)} = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
9190inteqd 4945 . . . . 5 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)} = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
92 onsuc 7792 . . . . . . 7 (𝑏 ∈ On → suc 𝑏 ∈ On)
93 naddov2 8673 . . . . . . 7 ((𝑎 ∈ On ∧ suc 𝑏 ∈ On) → (𝑎 +no suc 𝑏) = {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)})
9492, 93sylan2 592 . . . . . 6 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no suc 𝑏) = {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)})
9594adantr 480 . . . . 5 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → (𝑎 +no suc 𝑏) = {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)})
96 naddcl 8671 . . . . . . 7 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) ∈ On)
97 onsucmin 7802 . . . . . . 7 ((𝑎 +no 𝑏) ∈ On → suc (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
9896, 97syl 17 . . . . . 6 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → suc (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
9998adantr 480 . . . . 5 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → suc (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
10091, 95, 993eqtr4d 2774 . . . 4 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → (𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏))
101100ex 412 . . 3 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) → (𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏)))
10229, 101syld 47 . 2 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐𝑎𝑑𝑏 (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ∧ ∀𝑑𝑏 (𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑)) → (𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏)))
1035, 11, 16, 21, 27, 102on2ind 8663 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3053  {crab 3424  Vcvv 3466  cun 3938  {csn 4620   cuni 4899   cint 4940  Ord word 6353  Oncon0 6354  suc csuc 6356  (class class class)co 7401   +no cnadd 8659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-nadd 8660
This theorem is referenced by:  naddass1  42599  naddgeoa  42600  naddonnn  42601
  Copyright terms: Public domain W3C validator