| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no suc 𝑏 ) = ( 𝑐 +no suc 𝑏 ) ) |
| 2 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑏 ) = ( 𝑐 +no 𝑏 ) ) |
| 3 |
|
suceq |
⊢ ( ( 𝑎 +no 𝑏 ) = ( 𝑐 +no 𝑏 ) → suc ( 𝑎 +no 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) |
| 4 |
2 3
|
syl |
⊢ ( 𝑎 = 𝑐 → suc ( 𝑎 +no 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) |
| 5 |
1 4
|
eqeq12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no suc 𝑏 ) = suc ( 𝑎 +no 𝑏 ) ↔ ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ) |
| 6 |
|
suceq |
⊢ ( 𝑏 = 𝑑 → suc 𝑏 = suc 𝑑 ) |
| 7 |
6
|
oveq2d |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 +no suc 𝑏 ) = ( 𝑐 +no suc 𝑑 ) ) |
| 8 |
|
oveq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 +no 𝑏 ) = ( 𝑐 +no 𝑑 ) ) |
| 9 |
|
suceq |
⊢ ( ( 𝑐 +no 𝑏 ) = ( 𝑐 +no 𝑑 ) → suc ( 𝑐 +no 𝑏 ) = suc ( 𝑐 +no 𝑑 ) ) |
| 10 |
8 9
|
syl |
⊢ ( 𝑏 = 𝑑 → suc ( 𝑐 +no 𝑏 ) = suc ( 𝑐 +no 𝑑 ) ) |
| 11 |
7 10
|
eqeq12d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ↔ ( 𝑐 +no suc 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ) ) |
| 12 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no suc 𝑑 ) = ( 𝑐 +no suc 𝑑 ) ) |
| 13 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑑 ) = ( 𝑐 +no 𝑑 ) ) |
| 14 |
|
suceq |
⊢ ( ( 𝑎 +no 𝑑 ) = ( 𝑐 +no 𝑑 ) → suc ( 𝑎 +no 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ) |
| 15 |
13 14
|
syl |
⊢ ( 𝑎 = 𝑐 → suc ( 𝑎 +no 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ) |
| 16 |
12 15
|
eqeq12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no suc 𝑑 ) = suc ( 𝑎 +no 𝑑 ) ↔ ( 𝑐 +no suc 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ) ) |
| 17 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no suc 𝑏 ) = ( 𝐴 +no suc 𝑏 ) ) |
| 18 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) ) |
| 19 |
|
suceq |
⊢ ( ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) → suc ( 𝑎 +no 𝑏 ) = suc ( 𝐴 +no 𝑏 ) ) |
| 20 |
18 19
|
syl |
⊢ ( 𝑎 = 𝐴 → suc ( 𝑎 +no 𝑏 ) = suc ( 𝐴 +no 𝑏 ) ) |
| 21 |
17 20
|
eqeq12d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no suc 𝑏 ) = suc ( 𝑎 +no 𝑏 ) ↔ ( 𝐴 +no suc 𝑏 ) = suc ( 𝐴 +no 𝑏 ) ) ) |
| 22 |
|
suceq |
⊢ ( 𝑏 = 𝐵 → suc 𝑏 = suc 𝐵 ) |
| 23 |
22
|
oveq2d |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no suc 𝑏 ) = ( 𝐴 +no suc 𝐵 ) ) |
| 24 |
|
oveq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) ) |
| 25 |
|
suceq |
⊢ ( ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) → suc ( 𝐴 +no 𝑏 ) = suc ( 𝐴 +no 𝐵 ) ) |
| 26 |
24 25
|
syl |
⊢ ( 𝑏 = 𝐵 → suc ( 𝐴 +no 𝑏 ) = suc ( 𝐴 +no 𝐵 ) ) |
| 27 |
23 26
|
eqeq12d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 +no suc 𝑏 ) = suc ( 𝐴 +no 𝑏 ) ↔ ( 𝐴 +no suc 𝐵 ) = suc ( 𝐴 +no 𝐵 ) ) ) |
| 28 |
|
simp2 |
⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no suc 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no suc 𝑑 ) = suc ( 𝑎 +no 𝑑 ) ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) |
| 29 |
28
|
a1i |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no suc 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no suc 𝑑 ) = suc ( 𝑎 +no 𝑑 ) ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ) |
| 30 |
|
df-suc |
⊢ suc 𝑏 = ( 𝑏 ∪ { 𝑏 } ) |
| 31 |
30
|
a1i |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → suc 𝑏 = ( 𝑏 ∪ { 𝑏 } ) ) |
| 32 |
31
|
raleqdv |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ∈ ( 𝑏 ∪ { 𝑏 } ) ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ) |
| 33 |
|
vex |
⊢ 𝑏 ∈ V |
| 34 |
33
|
a1i |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → 𝑏 ∈ V ) |
| 35 |
|
oveq2 |
⊢ ( 𝑑 = 𝑏 → ( 𝑎 +no 𝑑 ) = ( 𝑎 +no 𝑏 ) ) |
| 36 |
35
|
eleq1d |
⊢ ( 𝑑 = 𝑏 → ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ) |
| 37 |
36
|
ralunsn |
⊢ ( 𝑏 ∈ V → ( ∀ 𝑑 ∈ ( 𝑏 ∪ { 𝑏 } ) ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ) ) |
| 38 |
34 37
|
syl |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑑 ∈ ( 𝑏 ∪ { 𝑏 } ) ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ) ) |
| 39 |
38
|
biancomd |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑑 ∈ ( 𝑏 ∪ { 𝑏 } ) ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ) ) |
| 40 |
32 39
|
bitrd |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ) ) |
| 41 |
|
nfv |
⊢ Ⅎ 𝑐 ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) |
| 42 |
|
nfra1 |
⊢ Ⅎ 𝑐 ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) |
| 43 |
41 42
|
nfan |
⊢ Ⅎ 𝑐 ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) |
| 44 |
|
nfv |
⊢ Ⅎ 𝑐 𝑥 ∈ On |
| 45 |
43 44
|
nfan |
⊢ Ⅎ 𝑐 ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) |
| 46 |
|
simplr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) |
| 47 |
46
|
r19.21bi |
⊢ ( ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) ∧ 𝑐 ∈ 𝑎 ) → ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) |
| 48 |
47
|
eleq1d |
⊢ ( ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) ∧ 𝑐 ∈ 𝑎 ) → ( ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ↔ suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) |
| 49 |
45 48
|
ralbida |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) |
| 50 |
40 49
|
anbi12d |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) ↔ ( ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) ) |
| 51 |
|
anass |
⊢ ( ( ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ↔ ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) ) |
| 52 |
|
simpll3 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑥 ∈ On ) |
| 53 |
|
simpr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ 𝑏 ) |
| 54 |
|
simpll2 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑏 ∈ On ) |
| 55 |
|
onelon |
⊢ ( ( 𝑏 ∈ On ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ On ) |
| 56 |
54 53 55
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ On ) |
| 57 |
|
simpll1 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑎 ∈ On ) |
| 58 |
|
naddel2 |
⊢ ( ( 𝑑 ∈ On ∧ 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑑 ∈ 𝑏 ↔ ( 𝑎 +no 𝑑 ) ∈ ( 𝑎 +no 𝑏 ) ) ) |
| 59 |
56 54 57 58
|
syl3anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑑 ∈ 𝑏 ↔ ( 𝑎 +no 𝑑 ) ∈ ( 𝑎 +no 𝑏 ) ) ) |
| 60 |
53 59
|
mpbid |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑎 +no 𝑑 ) ∈ ( 𝑎 +no 𝑏 ) ) |
| 61 |
|
simplr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) |
| 62 |
60 61
|
jca |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → ( ( 𝑎 +no 𝑑 ) ∈ ( 𝑎 +no 𝑏 ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ) |
| 63 |
|
ontr1 |
⊢ ( 𝑥 ∈ On → ( ( ( 𝑎 +no 𝑑 ) ∈ ( 𝑎 +no 𝑏 ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) → ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ) |
| 64 |
52 62 63
|
sylc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) |
| 65 |
64
|
ralrimiva |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) |
| 66 |
|
simpll1 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → 𝑎 ∈ On ) |
| 67 |
|
simpr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → 𝑐 ∈ 𝑎 ) |
| 68 |
|
onelon |
⊢ ( ( 𝑎 ∈ On ∧ 𝑐 ∈ 𝑎 ) → 𝑐 ∈ On ) |
| 69 |
66 67 68
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → 𝑐 ∈ On ) |
| 70 |
|
simpll2 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → 𝑏 ∈ On ) |
| 71 |
69 66 70
|
3jca |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → ( 𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On ) ) |
| 72 |
|
naddelim |
⊢ ( ( 𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑐 ∈ 𝑎 → ( 𝑐 +no 𝑏 ) ∈ ( 𝑎 +no 𝑏 ) ) ) |
| 73 |
71 67 72
|
sylc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → ( 𝑐 +no 𝑏 ) ∈ ( 𝑎 +no 𝑏 ) ) |
| 74 |
|
simplr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) |
| 75 |
|
elunii |
⊢ ( ( ( 𝑐 +no 𝑏 ) ∈ ( 𝑎 +no 𝑏 ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) → ( 𝑐 +no 𝑏 ) ∈ ∪ 𝑥 ) |
| 76 |
73 74 75
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → ( 𝑐 +no 𝑏 ) ∈ ∪ 𝑥 ) |
| 77 |
|
simpll3 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → 𝑥 ∈ On ) |
| 78 |
|
eloni |
⊢ ( 𝑥 ∈ On → Ord 𝑥 ) |
| 79 |
77 78
|
syl |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → Ord 𝑥 ) |
| 80 |
|
ordsucuniel |
⊢ ( Ord 𝑥 → ( ( 𝑐 +no 𝑏 ) ∈ ∪ 𝑥 ↔ suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) |
| 81 |
79 80
|
syl |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → ( ( 𝑐 +no 𝑏 ) ∈ ∪ 𝑥 ↔ suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) |
| 82 |
76 81
|
mpbid |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ∧ 𝑐 ∈ 𝑎 ) → suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) |
| 83 |
82
|
ralrimiva |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) → ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) |
| 84 |
65 83
|
jca |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) |
| 85 |
84
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) ) |
| 86 |
85
|
ad4ant124 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) ) |
| 87 |
86
|
pm4.71d |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ↔ ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ) ) ) |
| 88 |
51 87
|
bitr4id |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ( ( ( 𝑎 +no 𝑏 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ) ∧ ∀ 𝑐 ∈ 𝑎 suc ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ↔ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ) |
| 89 |
50 88
|
bitrd |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) ↔ ( 𝑎 +no 𝑏 ) ∈ 𝑥 ) ) |
| 90 |
89
|
rabbidva |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) → { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) } = { 𝑥 ∈ On ∣ ( 𝑎 +no 𝑏 ) ∈ 𝑥 } ) |
| 91 |
90
|
inteqd |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( 𝑎 +no 𝑏 ) ∈ 𝑥 } ) |
| 92 |
|
onsuc |
⊢ ( 𝑏 ∈ On → suc 𝑏 ∈ On ) |
| 93 |
|
naddov2 |
⊢ ( ( 𝑎 ∈ On ∧ suc 𝑏 ∈ On ) → ( 𝑎 +no suc 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) } ) |
| 94 |
92 93
|
sylan2 |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 +no suc 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) } ) |
| 95 |
94
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) → ( 𝑎 +no suc 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ suc 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) ∈ 𝑥 ) } ) |
| 96 |
|
naddcl |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 +no 𝑏 ) ∈ On ) |
| 97 |
|
onsucmin |
⊢ ( ( 𝑎 +no 𝑏 ) ∈ On → suc ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( 𝑎 +no 𝑏 ) ∈ 𝑥 } ) |
| 98 |
96 97
|
syl |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → suc ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( 𝑎 +no 𝑏 ) ∈ 𝑥 } ) |
| 99 |
98
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) → suc ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( 𝑎 +no 𝑏 ) ∈ 𝑥 } ) |
| 100 |
91 95 99
|
3eqtr4d |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ) → ( 𝑎 +no suc 𝑏 ) = suc ( 𝑎 +no 𝑏 ) ) |
| 101 |
100
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) → ( 𝑎 +no suc 𝑏 ) = suc ( 𝑎 +no 𝑏 ) ) ) |
| 102 |
29 101
|
syld |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no suc 𝑑 ) = suc ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no suc 𝑏 ) = suc ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no suc 𝑑 ) = suc ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +no suc 𝑏 ) = suc ( 𝑎 +no 𝑏 ) ) ) |
| 103 |
5 11 16 21 27 102
|
on2ind |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no suc 𝐵 ) = suc ( 𝐴 +no 𝐵 ) ) |