Step | Hyp | Ref
| Expression |
1 | | oveq1 7282 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑎 +s 0s ) = (𝑏 +s 0s )) |
2 | | id 22 |
. . 3
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
3 | 1, 2 | eqeq12d 2754 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑎 +s 0s ) = 𝑎 ↔ (𝑏 +s 0s ) = 𝑏)) |
4 | | oveq1 7282 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑎 +s 0s ) = (𝐴 +s 0s )) |
5 | | id 22 |
. . 3
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
6 | 4, 5 | eqeq12d 2754 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑎 +s 0s ) = 𝑎 ↔ (𝐴 +s 0s ) = 𝐴)) |
7 | | 0sno 34020 |
. . . . . 6
⊢ 0s
∈ No |
8 | | addsval 34126 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 0s ∈ No ) → (𝑎 +s 0s ) = (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘ 0s )𝑧 = (𝑎 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘ 0s )𝑧 = (𝑎 +s 𝑤)}))) |
9 | 7, 8 | mpan2 688 |
. . . . 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 4110 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ( L ‘𝑎) → 𝑦 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))) |
12 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → ∀𝑏 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) |
13 | | oveq1 7282 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑦 → (𝑏 +s 0s ) = (𝑦 +s 0s )) |
14 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑦 → 𝑏 = 𝑦) |
15 | 13, 14 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑦 → ((𝑏 +s 0s ) = 𝑏 ↔ (𝑦 +s 0s ) = 𝑦)) |
16 | 15 | rspcva 3559 |
. . . . . . . . . . . . 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 2749 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) ∧ 𝑦 ∈ ( L ‘𝑎)) → (𝑥 = (𝑦 +s 0s ) ↔ 𝑥 = 𝑦)) |
19 | | equcom 2021 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
20 | 18, 19 | bitrdi 287 |
. . . . . . . . . 10
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) ∧ 𝑦 ∈ ( L ‘𝑎)) → (𝑥 = (𝑦 +s 0s ) ↔ 𝑦 = 𝑥)) |
21 | 20 | rexbidva 3225 |
. . . . . . . . 9
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s ) ↔ ∃𝑦 ∈ ( L ‘𝑎)𝑦 = 𝑥)) |
22 | | risset 3194 |
. . . . . . . . 9
⊢ (𝑥 ∈ ( L ‘𝑎) ↔ ∃𝑦 ∈ ( L ‘𝑎)𝑦 = 𝑥) |
23 | 21, 22 | bitr4di 289 |
. . . . . . . 8
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s ) ↔ 𝑥 ∈ ( L ‘𝑎))) |
24 | 23 | abbi1dv 2878 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} = ( L ‘𝑎)) |
25 | | rex0 4291 |
. . . . . . . . . 10
⊢ ¬
∃𝑦 ∈ ∅
𝑧 = (𝑎 +s 𝑦) |
26 | | left0s 34075 |
. . . . . . . . . . 11
⊢ ( L
‘ 0s ) = ∅ |
27 | 26 | rexeqi 3347 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ ( L
‘ 0s )𝑧 = (𝑎 +s 𝑦) ↔ ∃𝑦 ∈ ∅ 𝑧 = (𝑎 +s 𝑦)) |
28 | 25, 27 | mtbir 323 |
. . . . . . . . 9
⊢ ¬
∃𝑦 ∈ ( L ‘
0s )𝑧 = (𝑎 +s 𝑦) |
29 | 28 | abf 4336 |
. . . . . . . 8
⊢ {𝑧 ∣ ∃𝑦 ∈ ( L ‘ 0s )𝑧 = (𝑎 +s 𝑦)} = ∅ |
30 | 29 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → {𝑧 ∣ ∃𝑦 ∈ ( L ‘ 0s )𝑧 = (𝑎 +s 𝑦)} = ∅) |
31 | 24, 30 | uneq12d 4098 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘ 0s )𝑧 = (𝑎 +s 𝑦)}) = (( L ‘𝑎) ∪ ∅)) |
32 | | un0 4324 |
. . . . . 6
⊢ (( L
‘𝑎) ∪ ∅) =
( L ‘𝑎) |
33 | 31, 32 | eqtrdi 2794 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘ 0s )𝑧 = (𝑎 +s 𝑦)}) = ( L ‘𝑎)) |
34 | | elun2 4111 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ( R ‘𝑎) → 𝑤 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))) |
35 | | oveq1 7282 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑤 → (𝑏 +s 0s ) = (𝑤 +s 0s )) |
36 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑤 → 𝑏 = 𝑤) |
37 | 35, 36 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑤 → ((𝑏 +s 0s ) = 𝑏 ↔ (𝑤 +s 0s ) = 𝑤)) |
38 | 37 | rspcva 3559 |
. . . . . . . . . . . . 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 2749 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) ∧ 𝑤 ∈ ( R ‘𝑎)) → (𝑥 = (𝑤 +s 0s ) ↔ 𝑥 = 𝑤)) |
41 | | equcom 2021 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 ↔ 𝑤 = 𝑥) |
42 | 40, 41 | bitrdi 287 |
. . . . . . . . . 10
⊢ (((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) ∧ 𝑤 ∈ ( R ‘𝑎)) → (𝑥 = (𝑤 +s 0s ) ↔ 𝑤 = 𝑥)) |
43 | 42 | rexbidva 3225 |
. . . . . . . . 9
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s ) ↔ ∃𝑤 ∈ ( R ‘𝑎)𝑤 = 𝑥)) |
44 | | risset 3194 |
. . . . . . . . 9
⊢ (𝑥 ∈ ( R ‘𝑎) ↔ ∃𝑤 ∈ ( R ‘𝑎)𝑤 = 𝑥) |
45 | 43, 44 | bitr4di 289 |
. . . . . . . 8
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s ) ↔ 𝑥 ∈ ( R ‘𝑎))) |
46 | 45 | abbi1dv 2878 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → {𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} = ( R ‘𝑎)) |
47 | | rex0 4291 |
. . . . . . . . . 10
⊢ ¬
∃𝑤 ∈ ∅
𝑧 = (𝑎 +s 𝑤) |
48 | | right0s 34076 |
. . . . . . . . . . 11
⊢ ( R
‘ 0s ) = ∅ |
49 | 48 | rexeqi 3347 |
. . . . . . . . . 10
⊢
(∃𝑤 ∈ ( R
‘ 0s )𝑧 = (𝑎 +s 𝑤) ↔ ∃𝑤 ∈ ∅ 𝑧 = (𝑎 +s 𝑤)) |
50 | 47, 49 | mtbir 323 |
. . . . . . . . 9
⊢ ¬
∃𝑤 ∈ ( R ‘
0s )𝑧 = (𝑎 +s 𝑤) |
51 | 50 | abf 4336 |
. . . . . . . 8
⊢ {𝑧 ∣ ∃𝑤 ∈ ( R ‘ 0s )𝑧 = (𝑎 +s 𝑤)} = ∅ |
52 | 51 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → {𝑧 ∣ ∃𝑤 ∈ ( R ‘ 0s )𝑧 = (𝑎 +s 𝑤)} = ∅) |
53 | 46, 52 | uneq12d 4098 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘ 0s )𝑧 = (𝑎 +s 𝑤)}) = (( R ‘𝑎) ∪ ∅)) |
54 | | un0 4324 |
. . . . . 6
⊢ (( R
‘𝑎) ∪ ∅) =
( R ‘𝑎) |
55 | 53, 54 | eqtrdi 2794 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘ 0s )𝑧 = (𝑎 +s 𝑤)}) = ( R ‘𝑎)) |
56 | 33, 55 | oveq12d 7293 |
. . . 4
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝑎)𝑥 = (𝑦 +s 0s )} ∪ {𝑧 ∣ ∃𝑦 ∈ ( L ‘ 0s )𝑧 = (𝑎 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑤 ∈ ( R ‘𝑎)𝑥 = (𝑤 +s 0s )} ∪ {𝑧 ∣ ∃𝑤 ∈ ( R ‘ 0s )𝑧 = (𝑎 +s 𝑤)})) = (( L ‘𝑎) |s ( R ‘𝑎))) |
57 | | lrcut 34083 |
. . . . 5
⊢ (𝑎 ∈
No → (( L ‘𝑎) |s ( R ‘𝑎)) = 𝑎) |
58 | 57 | adantr 481 |
. . . 4
⊢ ((𝑎 ∈
No ∧ ∀𝑏
∈ (( L ‘𝑎) ∪
( R ‘𝑎))(𝑏 +s 0s ) = 𝑏) → (( L ‘𝑎) |s ( R ‘𝑎)) = 𝑎) |
59 | 10, 56, 58 | 3eqtrd 2782 |
. . 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 34102 |
1
⊢ (𝐴 ∈
No → (𝐴 +s 0s
) = 𝐴) |