MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  naddsuc2 Structured version   Visualization version   GIF version

Theorem naddsuc2 8738
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 7438 . . 3 (𝑎 = 𝑐 → (𝑎 +no suc 𝑏) = (𝑐 +no suc 𝑏))
2 oveq1 7438 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
3 suceq 6452 . . . 4 ((𝑎 +no 𝑏) = (𝑐 +no 𝑏) → suc (𝑎 +no 𝑏) = suc (𝑐 +no 𝑏))
42, 3syl 17 . . 3 (𝑎 = 𝑐 → suc (𝑎 +no 𝑏) = suc (𝑐 +no 𝑏))
51, 4eqeq12d 2751 . 2 (𝑎 = 𝑐 → ((𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏) ↔ (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)))
6 suceq 6452 . . . 4 (𝑏 = 𝑑 → suc 𝑏 = suc 𝑑)
76oveq2d 7447 . . 3 (𝑏 = 𝑑 → (𝑐 +no suc 𝑏) = (𝑐 +no suc 𝑑))
8 oveq2 7439 . . . 4 (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
9 suceq 6452 . . . 4 ((𝑐 +no 𝑏) = (𝑐 +no 𝑑) → suc (𝑐 +no 𝑏) = suc (𝑐 +no 𝑑))
108, 9syl 17 . . 3 (𝑏 = 𝑑 → suc (𝑐 +no 𝑏) = suc (𝑐 +no 𝑑))
117, 10eqeq12d 2751 . 2 (𝑏 = 𝑑 → ((𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ↔ (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑)))
12 oveq1 7438 . . 3 (𝑎 = 𝑐 → (𝑎 +no suc 𝑑) = (𝑐 +no suc 𝑑))
13 oveq1 7438 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
14 suceq 6452 . . . 4 ((𝑎 +no 𝑑) = (𝑐 +no 𝑑) → suc (𝑎 +no 𝑑) = suc (𝑐 +no 𝑑))
1513, 14syl 17 . . 3 (𝑎 = 𝑐 → suc (𝑎 +no 𝑑) = suc (𝑐 +no 𝑑))
1612, 15eqeq12d 2751 . 2 (𝑎 = 𝑐 → ((𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑) ↔ (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑)))
17 oveq1 7438 . . 3 (𝑎 = 𝐴 → (𝑎 +no suc 𝑏) = (𝐴 +no suc 𝑏))
18 oveq1 7438 . . . 4 (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
19 suceq 6452 . . . 4 ((𝑎 +no 𝑏) = (𝐴 +no 𝑏) → suc (𝑎 +no 𝑏) = suc (𝐴 +no 𝑏))
2018, 19syl 17 . . 3 (𝑎 = 𝐴 → suc (𝑎 +no 𝑏) = suc (𝐴 +no 𝑏))
2117, 20eqeq12d 2751 . 2 (𝑎 = 𝐴 → ((𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏) ↔ (𝐴 +no suc 𝑏) = suc (𝐴 +no 𝑏)))
22 suceq 6452 . . . 4 (𝑏 = 𝐵 → suc 𝑏 = suc 𝐵)
2322oveq2d 7447 . . 3 (𝑏 = 𝐵 → (𝐴 +no suc 𝑏) = (𝐴 +no suc 𝐵))
24 oveq2 7439 . . . 4 (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
25 suceq 6452 . . . 4 ((𝐴 +no 𝑏) = (𝐴 +no 𝐵) → suc (𝐴 +no 𝑏) = suc (𝐴 +no 𝐵))
2624, 25syl 17 . . 3 (𝑏 = 𝐵 → suc (𝐴 +no 𝑏) = suc (𝐴 +no 𝐵))
2723, 26eqeq12d 2751 . 2 (𝑏 = 𝐵 → ((𝐴 +no suc 𝑏) = suc (𝐴 +no 𝑏) ↔ (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵)))
28 simp2 1136 . . . 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 6392 . . . . . . . . . . . 12 suc 𝑏 = (𝑏 ∪ {𝑏})
3130a1i 11 . . . . . . . . . . 11 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → suc 𝑏 = (𝑏 ∪ {𝑏}))
3231raleqdv 3324 . . . . . . . . . 10 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ↔ ∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥))
33 vex 3482 . . . . . . . . . . . . 13 𝑏 ∈ V
3433a1i 11 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → 𝑏 ∈ V)
35 oveq2 7439 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 → (𝑎 +no 𝑑) = (𝑎 +no 𝑏))
3635eleq1d 2824 . . . . . . . . . . . . 13 (𝑑 = 𝑏 → ((𝑎 +no 𝑑) ∈ 𝑥 ↔ (𝑎 +no 𝑏) ∈ 𝑥))
3736ralunsn 4899 . . . . . . . . . . . 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 1912 . . . . . . . . . . . 12 𝑐(𝑎 ∈ On ∧ 𝑏 ∈ On)
42 nfra1 3282 . . . . . . . . . . . 12 𝑐𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)
4341, 42nfan 1897 . . . . . . . . . . 11 𝑐((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
44 nfv 1912 . . . . . . . . . . 11 𝑐 𝑥 ∈ On
4543, 44nfan 1897 . . . . . . . . . 10 𝑐(((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On)
46 simplr 769 . . . . . . . . . . . 12 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
4746r19.21bi 3249 . . . . . . . . . . 11 (((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) ∧ 𝑐𝑎) → (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))
4847eleq1d 2824 . . . . . . . . . 10 (((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) ∧ 𝑐𝑎) → ((𝑐 +no suc 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥))
4945, 48ralbida 3268 . . . . . . . . 9 ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥 ↔ ∀𝑐𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))
5040, 49anbi12d 632 . . . . . . . 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 1213 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑥 ∈ On)
53 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑑𝑏)
54 simpll2 1212 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑏 ∈ On)
55 onelon 6411 . . . . . . . . . . . . . . . . . . 19 ((𝑏 ∈ On ∧ 𝑑𝑏) → 𝑑 ∈ On)
5654, 53, 55syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑑 ∈ On)
57 simpll1 1211 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → 𝑎 ∈ On)
58 naddel2 8725 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∈ On ∧ 𝑏 ∈ On ∧ 𝑎 ∈ On) → (𝑑𝑏 ↔ (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏)))
5956, 54, 57, 58syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑑𝑏 ↔ (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏)))
6053, 59mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏))
61 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑎 +no 𝑏) ∈ 𝑥)
6260, 61jca 511 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → ((𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥))
63 ontr1 6432 . . . . . . . . . . . . . . 15 (𝑥 ∈ On → (((𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (𝑎 +no 𝑑) ∈ 𝑥))
6452, 62, 63sylc 65 . . . . . . . . . . . . . 14 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑𝑏) → (𝑎 +no 𝑑) ∈ 𝑥)
6564ralrimiva 3144 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ 𝑥)
66 simpll1 1211 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑎 ∈ On)
67 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑐𝑎)
68 onelon 6411 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑐𝑎) → 𝑐 ∈ On)
6966, 67, 68syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑐 ∈ On)
70 simpll2 1212 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑏 ∈ On)
7169, 66, 703jca 1127 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On))
72 naddelim 8723 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑐𝑎 → (𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏)))
7371, 67, 72sylc 65 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏))
74 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑎 +no 𝑏) ∈ 𝑥)
75 elunii 4917 . . . . . . . . . . . . . . . 16 (((𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (𝑐 +no 𝑏) ∈ 𝑥)
7673, 74, 75syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → (𝑐 +no 𝑏) ∈ 𝑥)
77 simpll3 1213 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → 𝑥 ∈ On)
78 eloni 6396 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ On → Ord 𝑥)
7977, 78syl 17 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → Ord 𝑥)
80 ordsucuniel 7844 . . . . . . . . . . . . . . . 16 (Ord 𝑥 → ((𝑐 +no 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥))
8179, 80syl 17 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → ((𝑐 +no 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥))
8276, 81mpbid 232 . . . . . . . . . . . . . 14 ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐𝑎) → suc (𝑐 +no 𝑏) ∈ 𝑥)
8382ralrimiva 3144 . . . . . . . . . . . . 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 1172 . . . . . . . . . 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 3440 . . . . . 6 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)} = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
9190inteqd 4956 . . . . 5 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)} = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥})
92 onsuc 7831 . . . . . . 7 (𝑏 ∈ On → suc 𝑏 ∈ On)
93 naddov2 8716 . . . . . . 7 ((𝑎 ∈ On ∧ suc 𝑏 ∈ On) → (𝑎 +no suc 𝑏) = {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)})
9492, 93sylan2 593 . . . . . 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 8714 . . . . . . 7 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) ∈ On)
97 onsucmin 7841 . . . . . . 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 2785 . . . 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 8706 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wral 3059  {crab 3433  Vcvv 3478  cun 3961  {csn 4631   cuni 4912   cint 4951  Ord word 6385  Oncon0 6386  suc csuc 6388  (class class class)co 7431   +no cnadd 8702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-frecs 8305  df-nadd 8703
This theorem is referenced by:  naddoa  8739  naddass1  43383  naddgeoa  43384  naddonnn  43385
  Copyright terms: Public domain W3C validator