Step | Hyp | Ref
| Expression |
1 | | oveq1 7364 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑎 +s 0s ) = (𝑏 +s 0s
)) |
2 | | id 22 |
. . 3
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
3 | 1, 2 | eqeq12d 2752 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑎 +s 0s ) = 𝑎 ↔ (𝑏 +s 0s ) = 𝑏)) |
4 | | oveq1 7364 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑎 +s 0s ) = (𝐴 +s 0s
)) |
5 | | id 22 |
. . 3
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
6 | 4, 5 | eqeq12d 2752 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑎 +s 0s ) = 𝑎 ↔ (𝐴 +s 0s ) = 𝐴)) |
7 | | 0sno 27165 |
. . . . . 6
⊢
0s ∈ No |
8 | | addsval 27274 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 0s ∈ No ) →
(𝑎 +s
0s ) = (({𝑥
∣ ∃𝑦 ∈ ( L
‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)}))) |
9 | 7, 8 | mpan2 689 |
. . . . 5
⊢ (𝑎 ∈
No → (𝑎
+s 0s ) = (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)}))) |
10 | 9 | adantr 481 |
. . . 4
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (𝑎 +s 0s ) =
(({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)}))) |
11 | | elun1 4136 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ( L ‘𝑎) → 𝑦 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))) |
12 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → ∀𝑏 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) |
13 | | oveq1 7364 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑦 → (𝑏 +s 0s ) = (𝑦 +s 0s
)) |
14 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑦 → 𝑏 = 𝑦) |
15 | 13, 14 | eqeq12d 2752 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑦 → ((𝑏 +s 0s ) = 𝑏 ↔ (𝑦 +s 0s ) = 𝑦)) |
16 | 15 | rspcva 3579 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎)) ∧ ∀𝑏 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (𝑦 +s 0s ) = 𝑦) |
17 | 11, 12, 16 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) ∧ 𝑦 ∈ ( L ‘𝑎)) → (𝑦 +s 0s ) = 𝑦) |
18 | 17 | eqeq2d 2747 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) ∧ 𝑦 ∈ ( L ‘𝑎)) → (𝑥 = (𝑦 +s 0s ) ↔ 𝑥 = 𝑦)) |
19 | | equcom 2021 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
20 | 18, 19 | bitrdi 286 |
. . . . . . . . . 10
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) ∧ 𝑦 ∈ ( L ‘𝑎)) → (𝑥 = (𝑦 +s 0s ) ↔ 𝑦 = 𝑥)) |
21 | 20 | rexbidva 3173 |
. . . . . . . . 9
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s ) ↔
∃𝑦 ∈ ( L
‘𝑎)𝑦 = 𝑥)) |
22 | | risset 3221 |
. . . . . . . . 9
⊢ (𝑥 ∈ ( L ‘𝑎) ↔ ∃𝑦 ∈ ( L ‘𝑎)𝑦 = 𝑥) |
23 | 21, 22 | bitr4di 288 |
. . . . . . . 8
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s ) ↔ 𝑥 ∈ ( L ‘𝑎))) |
24 | 23 | abbi1dv 2872 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} = ( L
‘𝑎)) |
25 | | rex0 4317 |
. . . . . . . . . 10
⊢ ¬
∃𝑦 ∈ ∅
𝑧 = (𝑎 +s 𝑦) |
26 | | left0s 27222 |
. . . . . . . . . . 11
⊢ ( L
‘ 0s ) = ∅ |
27 | 26 | rexeqi 3312 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ ( L
‘ 0s )𝑧 =
(𝑎 +s 𝑦) ↔ ∃𝑦 ∈ ∅ 𝑧 = (𝑎 +s 𝑦)) |
28 | 25, 27 | mtbir 322 |
. . . . . . . . 9
⊢ ¬
∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦) |
29 | 28 | abf 4362 |
. . . . . . . 8
⊢ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)} = ∅ |
30 | 29 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)} = ∅) |
31 | 24, 30 | uneq12d 4124 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)}) = (( L ‘𝑎) ∪
∅)) |
32 | | un0 4350 |
. . . . . 6
⊢ (( L
‘𝑎) ∪ ∅) =
( L ‘𝑎) |
33 | 31, 32 | eqtrdi 2792 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)}) = ( L ‘𝑎)) |
34 | | elun2 4137 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ( R ‘𝑎) → 𝑤 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))) |
35 | | oveq1 7364 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑤 → (𝑏 +s 0s ) = (𝑤 +s 0s
)) |
36 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑤 → 𝑏 = 𝑤) |
37 | 35, 36 | eqeq12d 2752 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑤 → ((𝑏 +s 0s ) = 𝑏 ↔ (𝑤 +s 0s ) = 𝑤)) |
38 | 37 | rspcva 3579 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎)) ∧ ∀𝑏 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (𝑤 +s 0s ) = 𝑤) |
39 | 34, 12, 38 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) ∧ 𝑤 ∈ ( R ‘𝑎)) → (𝑤 +s 0s ) = 𝑤) |
40 | 39 | eqeq2d 2747 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) ∧ 𝑤 ∈ ( R ‘𝑎)) → (𝑥 = (𝑤 +s 0s ) ↔ 𝑥 = 𝑤)) |
41 | | equcom 2021 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 ↔ 𝑤 = 𝑥) |
42 | 40, 41 | bitrdi 286 |
. . . . . . . . . 10
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) ∧ 𝑤 ∈ ( R ‘𝑎)) → (𝑥 = (𝑤 +s 0s ) ↔ 𝑤 = 𝑥)) |
43 | 42 | rexbidva 3173 |
. . . . . . . . 9
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s ) ↔
∃𝑤 ∈ ( R
‘𝑎)𝑤 = 𝑥)) |
44 | | risset 3221 |
. . . . . . . . 9
⊢ (𝑥 ∈ ( R ‘𝑎) ↔ ∃𝑤 ∈ ( R ‘𝑎)𝑤 = 𝑥) |
45 | 43, 44 | bitr4di 288 |
. . . . . . . 8
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s ) ↔ 𝑥 ∈ ( R ‘𝑎))) |
46 | 45 | abbi1dv 2872 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → {𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} = ( R
‘𝑎)) |
47 | | rex0 4317 |
. . . . . . . . . 10
⊢ ¬
∃𝑤 ∈ ∅
𝑧 = (𝑎 +s 𝑤) |
48 | | right0s 27223 |
. . . . . . . . . . 11
⊢ ( R
‘ 0s ) = ∅ |
49 | 48 | rexeqi 3312 |
. . . . . . . . . 10
⊢
(∃𝑤 ∈ ( R
‘ 0s )𝑧 =
(𝑎 +s 𝑤) ↔ ∃𝑤 ∈ ∅ 𝑧 = (𝑎 +s 𝑤)) |
50 | 47, 49 | mtbir 322 |
. . . . . . . . 9
⊢ ¬
∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤) |
51 | 50 | abf 4362 |
. . . . . . . 8
⊢ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)} = ∅ |
52 | 51 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)} = ∅) |
53 | 46, 52 | uneq12d 4124 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)}) = (( R ‘𝑎) ∪
∅)) |
54 | | un0 4350 |
. . . . . 6
⊢ (( R
‘𝑎) ∪ ∅) =
( R ‘𝑎) |
55 | 53, 54 | eqtrdi 2792 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)}) = ( R ‘𝑎)) |
56 | 33, 55 | oveq12d 7375 |
. . . 4
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤)})) = (( L ‘𝑎) |s ( R ‘𝑎))) |
57 | | lrcut 27232 |
. . . . 5
⊢ (𝑎 ∈
No → (( L ‘𝑎) |s ( R ‘𝑎)) = 𝑎) |
58 | 57 | adantr 481 |
. . . 4
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (( L ‘𝑎) |s ( R ‘𝑎)) = 𝑎) |
59 | 10, 56, 58 | 3eqtrd 2780 |
. . 3
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) =
𝑏) → (𝑎 +s 0s ) =
𝑎) |
60 | 59 | ex 413 |
. 2
⊢ (𝑎 ∈
No → (∀𝑏 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))(𝑏 +s 0s ) = 𝑏 → (𝑎 +s 0s ) = 𝑎)) |
61 | 3, 6, 60 | noinds 27257 |
1
⊢ (𝐴 ∈
No → (𝐴
+s 0s ) = 𝐴) |