Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ (𝑥 = 𝑥O → 𝑥 = 𝑥O) |
2 | | fveq2 6839 |
. . . 4
⊢ (𝑥 = 𝑥O → ( -us ‘𝑥) = ( -us ‘𝑥O)) |
3 | 1, 2 | oveq12d 7369 |
. . 3
⊢ (𝑥 = 𝑥O → (𝑥 +s ( -us ‘𝑥)) = (𝑥O +s ( -us ‘𝑥O))) |
4 | 3 | eqeq1d 2739 |
. 2
⊢ (𝑥 = 𝑥O → ((𝑥 +s ( -us ‘𝑥)) = 0s ↔ (𝑥O +s ( -us ‘𝑥O)) = 0s
)) |
5 | | id 22 |
. . . 4
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
6 | | fveq2 6839 |
. . . 4
⊢ (𝑥 = 𝐴 → ( -us ‘𝑥) = ( -us ‘𝐴)) |
7 | 5, 6 | oveq12d 7369 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 +s ( -us ‘𝑥)) = (𝐴 +s ( -us ‘𝐴))) |
8 | 7 | eqeq1d 2739 |
. 2
⊢ (𝑥 = 𝐴 → ((𝑥 +s ( -us ‘𝑥)) = 0s ↔ (𝐴 +s ( -us ‘𝐴)) = 0s )) |
9 | | lltropt 27153 |
. . . . . 6
⊢ (𝑥 ∈
No → ( L ‘𝑥) <<s ( R ‘𝑥)) |
10 | 9 | adantr 481 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ( L
‘𝑥) <<s ( R
‘𝑥)) |
11 | | negscut2 34326 |
. . . . . 6
⊢ (𝑥 ∈
No → ( -us “ ( R ‘𝑥)) <<s ( -us “ ( L ‘𝑥))) |
12 | 11 | adantr 481 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (
-us “ ( R ‘𝑥))
<<s ( -us “ ( L ‘𝑥))) |
13 | | lrcut 27180 |
. . . . . . 7
⊢ (𝑥 ∈
No → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥) |
14 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ((
L ‘𝑥) |s ( R
‘𝑥)) = 𝑥) |
15 | 14 | eqcomd 2743 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
𝑥 = (( L ‘𝑥) |s ( R ‘𝑥))) |
16 | | negsval 34312 |
. . . . . 6
⊢ (𝑥 ∈
No → ( -us ‘𝑥) = (( -us “ ( R ‘𝑥)) |s ( -us “ ( L
‘𝑥)))) |
17 | 16 | adantr 481 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (
-us ‘𝑥) = (( -us
“ ( R ‘𝑥)) |s (
-us “ ( L ‘𝑥)))) |
18 | 10, 12, 15, 17 | addsunif 34300 |
. . . 4
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(𝑥 +s ( -us ‘𝑥)) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)}))) |
19 | | negsfn 34310 |
. . . . . . . . 9
⊢ -us Fn
No |
20 | | rightssno 27161 |
. . . . . . . . 9
⊢ ( R
‘𝑥) ⊆ No |
21 | | oveq2 7359 |
. . . . . . . . . . 11
⊢ (𝑝 = ( -us ‘𝑥R) → (𝑥 +s 𝑝) = (𝑥 +s ( -us ‘𝑥R))) |
22 | 21 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑝 = ( -us ‘𝑥R) → (𝑏 = (𝑥 +s 𝑝) ↔ 𝑏 = (𝑥 +s ( -us ‘𝑥R)))) |
23 | 22 | imaeqsexv 34104 |
. . . . . . . . 9
⊢ (( -us Fn
No ∧ ( R ‘𝑥) ⊆ No )
→ (∃𝑝 ∈ (
-us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R)))) |
24 | 19, 20, 23 | mp2an 690 |
. . . . . . . 8
⊢
(∃𝑝 ∈ (
-us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))) |
25 | 24 | abbii 2807 |
. . . . . . 7
⊢ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R
‘𝑥))𝑏 = (𝑥 +s 𝑝)} = {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} |
26 | 25 | uneq2i 4118 |
. . . . . 6
⊢ ({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) = ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) |
27 | | leftssno 27160 |
. . . . . . . . 9
⊢ ( L
‘𝑥) ⊆ No |
28 | | oveq2 7359 |
. . . . . . . . . . 11
⊢ (𝑞 = ( -us ‘𝑥L) → (𝑥 +s 𝑞) = (𝑥 +s ( -us ‘𝑥L))) |
29 | 28 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑞 = ( -us ‘𝑥L) → (𝑑 = (𝑥 +s 𝑞) ↔ 𝑑 = (𝑥 +s ( -us ‘𝑥L)))) |
30 | 29 | imaeqsexv 34104 |
. . . . . . . . 9
⊢ (( -us Fn
No ∧ ( L ‘𝑥) ⊆ No )
→ (∃𝑞 ∈ (
-us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L)))) |
31 | 19, 27, 30 | mp2an 690 |
. . . . . . . 8
⊢
(∃𝑞 ∈ (
-us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))) |
32 | 31 | abbii 2807 |
. . . . . . 7
⊢ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L
‘𝑥))𝑑 = (𝑥 +s 𝑞)} = {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} |
33 | 32 | uneq2i 4118 |
. . . . . 6
⊢ ({𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)}) = ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) |
34 | 26, 33 | oveq12i 7363 |
. . . . 5
⊢ (({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)})) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) |
35 | | fvex 6852 |
. . . . . . . . . 10
⊢ ( L
‘𝑥) ∈
V |
36 | 35 | abrexex 7887 |
. . . . . . . . 9
⊢ {𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∈ V |
37 | | fvex 6852 |
. . . . . . . . . 10
⊢ ( R
‘𝑥) ∈
V |
38 | 37 | abrexex 7887 |
. . . . . . . . 9
⊢ {𝑏 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} ∈ V |
39 | 36, 38 | unex 7672 |
. . . . . . . 8
⊢ ({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∈ V |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∈ V) |
41 | | snex 5386 |
. . . . . . . 8
⊢ { 0s }
∈ V |
42 | 41 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {
0s } ∈ V) |
43 | 27 | sseli 3938 |
. . . . . . . . . . . . 13
⊢ (𝑥L ∈ ( L
‘𝑥) → 𝑥L ∈ No ) |
44 | 43 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → 𝑥L ∈ No ) |
45 | | simpll 765 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → 𝑥 ∈
No ) |
46 | 45 | negscld 34323 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → ( -us
‘𝑥) ∈ No ) |
47 | 44, 46 | addscld 34286 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L +s ( -us
‘𝑥)) ∈ No ) |
48 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥L +s ( -us ‘𝑥)) → (𝑎 ∈ No
↔ (𝑥L +s (
-us ‘𝑥)) ∈ No )) |
49 | 47, 48 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑎 = (𝑥L +s ( -us ‘𝑥)) → 𝑎 ∈ No
)) |
50 | 49 | rexlimdva 3150 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥L
∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥)) → 𝑎 ∈ No
)) |
51 | 50 | abssdv 4023 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
{𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ⊆ No ) |
52 | | simpll 765 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → 𝑥 ∈
No ) |
53 | 20 | sseli 3938 |
. . . . . . . . . . . . . 14
⊢ (𝑥R ∈ ( R
‘𝑥) → 𝑥R ∈ No ) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → 𝑥R ∈ No ) |
55 | 54 | negscld 34323 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → ( -us
‘𝑥R)
∈ No ) |
56 | 52, 55 | addscld 34286 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥 +s ( -us ‘𝑥R)) ∈ No ) |
57 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑥 +s ( -us ‘𝑥R)) → (𝑏 ∈ No
↔ (𝑥 +s ( -us
‘𝑥R))
∈ No )) |
58 | 56, 57 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑏 = (𝑥 +s ( -us ‘𝑥R)) → 𝑏 ∈ No
)) |
59 | 58 | rexlimdva 3150 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥R
∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R)) → 𝑏 ∈ No
)) |
60 | 59 | abssdv 4023 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
{𝑏 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} ⊆ No ) |
61 | 51, 60 | unssd 4144 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ⊆ No ) |
62 | | 0sno 27116 |
. . . . . . . 8
⊢ 0s
∈ No |
63 | | snssi 4766 |
. . . . . . . 8
⊢ ( 0s
∈ No → { 0s } ⊆ No ) |
64 | 62, 63 | mp1i 13 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {
0s } ⊆ No ) |
65 | | elun 4106 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ↔ (𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∨ 𝑝 ∈ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))})) |
66 | | vex 3447 |
. . . . . . . . . . . . 13
⊢ 𝑝 ∈ V |
67 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑝 → (𝑎 = (𝑥L +s ( -us ‘𝑥)) ↔ 𝑝 = (𝑥L +s ( -us ‘𝑥)))) |
68 | 67 | rexbidv 3173 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑝 → (∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥)) ↔ ∃𝑥L ∈ ( L
‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)))) |
69 | 66, 68 | elab 3628 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ↔ ∃𝑥L ∈ ( L
‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥))) |
70 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑝 → (𝑏 = (𝑥 +s ( -us ‘𝑥R)) ↔ 𝑝 = (𝑥 +s ( -us ‘𝑥R)))) |
71 | 70 | rexbidv 3173 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑝 → (∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R)) ↔ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) |
72 | 66, 71 | elab 3628 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} ↔ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) |
73 | 69, 72 | orbi12i 913 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∨ 𝑝 ∈ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ↔ (∃𝑥L ∈ ( L
‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) |
74 | 65, 73 | bitri 274 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ↔ (∃𝑥L ∈ ( L
‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) |
75 | | velsn 4600 |
. . . . . . . . . 10
⊢ (𝑞 ∈ { 0s } ↔ 𝑞 = 0s ) |
76 | 74, 75 | anbi12i 627 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∧ 𝑞 ∈ { 0s }) ↔ ((∃𝑥L ∈ ( L
‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) ∧ 𝑞 = 0s )) |
77 | | leftval 27144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( L
‘𝑥) = {𝑥L ∈ ( O
‘( bday ‘𝑥)) ∣ 𝑥L <s 𝑥} |
78 | 77 | rabeq2i 3427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥L ∈ ( L
‘𝑥) ↔ (𝑥L ∈ ( O
‘( bday ‘𝑥)) ∧ 𝑥L <s 𝑥)) |
79 | 78 | simprbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥L ∈ ( L
‘𝑥) → 𝑥L <s 𝑥) |
80 | 79 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → 𝑥L <s 𝑥) |
81 | | sltnegim 34324 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥L ∈ No ∧ 𝑥 ∈ No )
→ (𝑥L <s
𝑥 → ( -us ‘𝑥) <s ( -us ‘𝑥L))) |
82 | 44, 45, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L <s 𝑥 → ( -us ‘𝑥) <s ( -us ‘𝑥L))) |
83 | 80, 82 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → ( -us
‘𝑥) <s ( -us
‘𝑥L)) |
84 | 44 | negscld 34323 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → ( -us
‘𝑥L)
∈ No ) |
85 | | sltadd2 34296 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( -us
‘𝑥) ∈ No ∧ ( -us ‘𝑥L) ∈
No ∧ 𝑥L ∈ No
) → (( -us ‘𝑥) <s ( -us ‘𝑥L) ↔ (𝑥L +s ( -us ‘𝑥)) <s (𝑥L +s ( -us ‘𝑥L)))) |
86 | 46, 84, 44, 85 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (( -us
‘𝑥) <s ( -us
‘𝑥L)
↔ (𝑥L +s (
-us ‘𝑥)) <s (𝑥L +s ( -us
‘𝑥L)))) |
87 | 83, 86 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L +s ( -us
‘𝑥)) <s (𝑥L +s ( -us
‘𝑥L))) |
88 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥O = 𝑥L → 𝑥O = 𝑥L) |
89 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥O = 𝑥L → ( -us
‘𝑥O) = (
-us ‘𝑥L)) |
90 | 88, 89 | oveq12d 7369 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥O = 𝑥L → (𝑥O +s ( -us
‘𝑥O)) =
(𝑥L +s ( -us
‘𝑥L))) |
91 | 90 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥O = 𝑥L → ((𝑥O +s ( -us
‘𝑥O)) = 0s
↔ (𝑥L +s (
-us ‘𝑥L))
= 0s )) |
92 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) →
∀𝑥O
∈ (( L ‘𝑥) ∪
( R ‘𝑥))(𝑥O +s ( -us
‘𝑥O)) = 0s
) |
93 | | elun1 4134 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥L ∈ ( L
‘𝑥) → 𝑥L ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
94 | 93 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → 𝑥L ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
95 | 91, 92, 94 | rspcdva 3580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L +s ( -us
‘𝑥L)) = 0s
) |
96 | 87, 95 | breqtrd 5129 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L +s ( -us
‘𝑥)) <s 0s
) |
97 | | breq1 5106 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = (𝑥L +s ( -us ‘𝑥)) → (𝑝 <s 0s ↔ (𝑥L +s ( -us ‘𝑥)) <s 0s )) |
98 | 96, 97 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑝 = (𝑥L +s ( -us ‘𝑥)) → 𝑝 <s 0s )) |
99 | 98 | rexlimdva 3150 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥L
∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) → 𝑝 <s 0s )) |
100 | 99 | imp 407 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
∃𝑥L ∈
( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥))) → 𝑝 <s 0s ) |
101 | | rightval 27145 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( R
‘𝑥) = {𝑥R ∈ ( O
‘( bday ‘𝑥)) ∣ 𝑥 <s 𝑥R} |
102 | 101 | rabeq2i 3427 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥R ∈ ( R
‘𝑥) ↔ (𝑥R ∈ ( O
‘( bday ‘𝑥)) ∧ 𝑥 <s 𝑥R)) |
103 | 102 | simprbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥R ∈ ( R
‘𝑥) → 𝑥 <s 𝑥R) |
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → 𝑥 <s 𝑥R) |
105 | | sltadd1 34297 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
No ∧ 𝑥R ∈ No
∧ ( -us ‘𝑥R) ∈
No ) → (𝑥 <s
𝑥R ↔ (𝑥 +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us
‘𝑥R)))) |
106 | 52, 54, 55, 105 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥 <s 𝑥R ↔ (𝑥 +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥R)))) |
107 | 104, 106 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥 +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us
‘𝑥R))) |
108 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥O = 𝑥R → 𝑥O = 𝑥R) |
109 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥O = 𝑥R → ( -us
‘𝑥O) = (
-us ‘𝑥R)) |
110 | 108, 109 | oveq12d 7369 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥O = 𝑥R → (𝑥O +s ( -us
‘𝑥O)) =
(𝑥R +s ( -us
‘𝑥R))) |
111 | 110 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥O = 𝑥R → ((𝑥O +s ( -us
‘𝑥O)) = 0s
↔ (𝑥R +s (
-us ‘𝑥R))
= 0s )) |
112 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) →
∀𝑥O
∈ (( L ‘𝑥) ∪
( R ‘𝑥))(𝑥O +s ( -us
‘𝑥O)) = 0s
) |
113 | | elun2 4135 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥R ∈ ( R
‘𝑥) → 𝑥R ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
114 | 113 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → 𝑥R ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
115 | 111, 112,
114 | rspcdva 3580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥R +s ( -us
‘𝑥R)) = 0s
) |
116 | 107, 115 | breqtrd 5129 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥 +s ( -us ‘𝑥R)) <s 0s
) |
117 | | breq1 5106 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = (𝑥 +s ( -us ‘𝑥R)) → (𝑝 <s 0s ↔ (𝑥 +s ( -us ‘𝑥R)) <s 0s )) |
118 | 116, 117 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑝 = (𝑥 +s ( -us ‘𝑥R)) → 𝑝 <s 0s )) |
119 | 118 | rexlimdva 3150 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥R
∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)) → 𝑝 <s 0s )) |
120 | 119 | imp 407 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
∃𝑥R ∈
( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) → 𝑝 <s 0s ) |
121 | 100, 120 | jaodan 956 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
(∃𝑥L
∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) → 𝑝 <s 0s ) |
122 | | breq2 5107 |
. . . . . . . . . . 11
⊢ (𝑞 = 0s → (𝑝 <s 𝑞 ↔ 𝑝 <s 0s )) |
123 | 121, 122 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
(∃𝑥L
∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) → (𝑞 = 0s → 𝑝 <s 𝑞)) |
124 | 123 | expimpd 454 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(((∃𝑥L
∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R
‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) ∧ 𝑞 = 0s ) → 𝑝 <s 𝑞)) |
125 | 76, 124 | biimtrid 241 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
((𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∧ 𝑞 ∈ { 0s }) → 𝑝 <s 𝑞)) |
126 | 125 | 3impib 1116 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∧ 𝑞 ∈ { 0s }) → 𝑝 <s 𝑞) |
127 | 40, 42, 61, 64, 126 | ssltd 27082 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) <<s { 0s
}) |
128 | 37 | abrexex 7887 |
. . . . . . . . 9
⊢ {𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∈ V |
129 | 35 | abrexex 7887 |
. . . . . . . . 9
⊢ {𝑑 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} ∈ V |
130 | 128, 129 | unex 7672 |
. . . . . . . 8
⊢ ({𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ∈ V |
131 | 130 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
({𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ∈ V) |
132 | 52 | negscld 34323 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → ( -us
‘𝑥) ∈ No ) |
133 | 54, 132 | addscld 34286 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥R +s ( -us
‘𝑥)) ∈ No ) |
134 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝑥R +s ( -us ‘𝑥)) → (𝑐 ∈ No
↔ (𝑥R +s (
-us ‘𝑥)) ∈ No )) |
135 | 133, 134 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑐 = (𝑥R +s ( -us ‘𝑥)) → 𝑐 ∈ No
)) |
136 | 135 | rexlimdva 3150 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥R
∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥)) → 𝑐 ∈ No
)) |
137 | 136 | abssdv 4023 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
{𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ⊆ No ) |
138 | 45, 84 | addscld 34286 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥 +s ( -us ‘𝑥L)) ∈ No ) |
139 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑑 = (𝑥 +s ( -us ‘𝑥L)) → (𝑑 ∈ No
↔ (𝑥 +s ( -us
‘𝑥L))
∈ No )) |
140 | 138, 139 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑑 = (𝑥 +s ( -us ‘𝑥L)) → 𝑑 ∈ No
)) |
141 | 140 | rexlimdva 3150 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥L
∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L)) → 𝑑 ∈ No
)) |
142 | 141 | abssdv 4023 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
{𝑑 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} ⊆ No ) |
143 | 137, 142 | unssd 4144 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
({𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ⊆ No ) |
144 | | velsn 4600 |
. . . . . . . . . 10
⊢ (𝑝 ∈ { 0s } ↔ 𝑝 = 0s ) |
145 | | elun 4106 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ↔ (𝑞 ∈ {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∨ 𝑞 ∈ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) |
146 | | vex 3447 |
. . . . . . . . . . . . 13
⊢ 𝑞 ∈ V |
147 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑞 → (𝑐 = (𝑥R +s ( -us ‘𝑥)) ↔ 𝑞 = (𝑥R +s ( -us ‘𝑥)))) |
148 | 147 | rexbidv 3173 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑞 → (∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥)) ↔ ∃𝑥R ∈ ( R
‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)))) |
149 | 146, 148 | elab 3628 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ↔ ∃𝑥R ∈ ( R
‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥))) |
150 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑞 → (𝑑 = (𝑥 +s ( -us ‘𝑥L)) ↔ 𝑞 = (𝑥 +s ( -us ‘𝑥L)))) |
151 | 150 | rexbidv 3173 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑞 → (∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L)) ↔ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) |
152 | 146, 151 | elab 3628 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} ↔ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))) |
153 | 149, 152 | orbi12i 913 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∨ 𝑞 ∈ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ↔ (∃𝑥R ∈ ( R
‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) |
154 | 145, 153 | bitri 274 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ↔ (∃𝑥R ∈ ( R
‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) |
155 | 144, 154 | anbi12i 627 |
. . . . . . . . 9
⊢ ((𝑝 ∈ { 0s } ∧ 𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) ↔ (𝑝 = 0s ∧ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))))) |
156 | | sltnegim 34324 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈
No ∧ 𝑥R ∈ No
) → (𝑥 <s
𝑥R → ( -us
‘𝑥R) <s
( -us ‘𝑥))) |
157 | 52, 54, 156 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥 <s 𝑥R → ( -us ‘𝑥R) <s ( -us
‘𝑥))) |
158 | 104, 157 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → ( -us
‘𝑥R) <s
( -us ‘𝑥)) |
159 | | sltadd2 34296 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((( -us
‘𝑥R)
∈ No ∧ ( -us ‘𝑥) ∈ No
∧ 𝑥R ∈
No ) → (( -us ‘𝑥R) <s ( -us ‘𝑥) ↔ (𝑥R +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us
‘𝑥)))) |
160 | 55, 132, 54, 159 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (( -us
‘𝑥R) <s
( -us ‘𝑥) ↔
(𝑥R +s ( -us
‘𝑥R))
<s (𝑥R +s (
-us ‘𝑥)))) |
161 | 158, 160 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑥R +s ( -us
‘𝑥R))
<s (𝑥R +s (
-us ‘𝑥))) |
162 | 115, 161 | eqbrtrrd 5127 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → 0s <s
(𝑥R +s ( -us
‘𝑥))) |
163 | | breq2 5107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = (𝑥R +s ( -us ‘𝑥)) → ( 0s <s 𝑞 ↔ 0s <s (𝑥R +s ( -us
‘𝑥)))) |
164 | 162, 163 | syl5ibrcom 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥R ∈ ( R
‘𝑥)) → (𝑞 = (𝑥R +s ( -us ‘𝑥)) → 0s <s 𝑞)) |
165 | 164 | rexlimdva 3150 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥R
∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) → 0s <s 𝑞)) |
166 | 165 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
∃𝑥R ∈
( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥))) → 0s <s 𝑞) |
167 | | sltadd1 34297 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥L ∈ No ∧ 𝑥 ∈ No
∧ ( -us ‘𝑥L) ∈
No ) → (𝑥L <s 𝑥 ↔ (𝑥L +s ( -us ‘𝑥L)) <s (𝑥 +s ( -us ‘𝑥L)))) |
168 | 44, 45, 84, 167 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L <s 𝑥 ↔ (𝑥L +s ( -us ‘𝑥L)) <s (𝑥 +s ( -us ‘𝑥L)))) |
169 | 80, 168 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑥L +s ( -us
‘𝑥L))
<s (𝑥 +s ( -us
‘𝑥L))) |
170 | 95, 169 | eqbrtrrd 5127 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → 0s <s
(𝑥 +s ( -us ‘𝑥L))) |
171 | | breq2 5107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = (𝑥 +s ( -us ‘𝑥L)) → ( 0s <s 𝑞 ↔ 0s <s (𝑥 +s ( -us ‘𝑥L)))) |
172 | 170, 171 | syl5ibrcom 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑥L ∈ ( L
‘𝑥)) → (𝑞 = (𝑥 +s ( -us ‘𝑥L)) → 0s <s 𝑞)) |
173 | 172 | rexlimdva 3150 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(∃𝑥L
∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)) → 0s <s 𝑞)) |
174 | 173 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
∃𝑥L ∈
( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))) → 0s <s 𝑞) |
175 | 166, 174 | jaodan 956 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
(∃𝑥R
∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) → 0s <s 𝑞) |
176 | | breq1 5106 |
. . . . . . . . . . . 12
⊢ (𝑝 = 0s → (𝑝 <s 𝑞 ↔ 0s <s 𝑞)) |
177 | 175, 176 | syl5ibrcom 246 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
(∃𝑥R
∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) → (𝑝 = 0s → 𝑝 <s 𝑞)) |
178 | 177 | ex 413 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
((∃𝑥R
∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))) → (𝑝 = 0s → 𝑝 <s 𝑞))) |
179 | 178 | impcomd 412 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
((𝑝 = 0s ∧
(∃𝑥R
∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L
‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) → 𝑝 <s 𝑞)) |
180 | 155, 179 | biimtrid 241 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
((𝑝 ∈ { 0s } ∧
𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) → 𝑝 <s 𝑞)) |
181 | 180 | 3impib 1116 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧
𝑝 ∈ { 0s } ∧ 𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) → 𝑝 <s 𝑞) |
182 | 42, 131, 64, 143, 181 | ssltd 27082 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {
0s } <<s ({𝑐 ∣
∃𝑥R ∈
( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) |
183 | 127, 182 | cuteq0 27122 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) = 0s ) |
184 | 34, 183 | eqtrid 2789 |
. . . 4
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)})) = 0s ) |
185 | 18, 184 | eqtrd 2777 |
. . 3
⊢ ((𝑥 ∈
No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) →
(𝑥 +s ( -us ‘𝑥)) = 0s ) |
186 | 185 | ex 413 |
. 2
⊢ (𝑥 ∈
No → (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s →
(𝑥 +s ( -us ‘𝑥)) = 0s )) |
187 | 4, 8, 186 | noinds 34253 |
1
⊢ (𝐴 ∈
No → (𝐴 +s (
-us ‘𝐴)) = 0s
) |